MeasureTheory.Function.HasFiniteIntegral

コード元 MeasureTheory.Function.HasFiniteIntegral

variable [ENorm ε]

/-- `HasFiniteIntegral f μ` means that the integral `∫⁻ a, ‖f a‖ ∂μ` is finite.
  `HasFiniteIntegral f` means `HasFiniteIntegral f volume`. -/
def HasFiniteIntegral {_ : MeasurableSpace α} (f : α → ε)
    (μ : Measure α := by volume_tac) : Prop :=
  ∫⁻ a, ‖f a‖ₑ ∂μ < ∞

ここで, ‖ e ‖ₑはeの拡張(extended, ∞を含む)非負実数ノルムで以下のように定義されます.

/-- Auxiliary class, endowing a type `α` with a function `enorm : α → ℝ≥0∞` with notation `‖x‖ₑ`. -/
@[notation_class]
class ENorm (E : Type*) where
  /-- the `ℝ≥0∞`-valued norm function. -/
  enorm : E → ℝ≥0∞

@[inherit_doc] notation "‖" e "‖ₑ" => enorm e

variable [NormedAddCommGroup β]

theorem hasFiniteIntegral_iff_norm (f : α → β) :
    HasFiniteIntegral f μ ↔ (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) < ∞ := by
  simp only [hasFiniteIntegral_iff_enorm, ofReal_norm_eq_enorm]

fの値域がNormedAddCommGroup(ノルム付き可換群)である時, HasFiniteIntegralはfのノルムの絶対可積分性と同値です. これは以下のofReal_norm_eq_enormから従います. ここで@[to_additive ofReal_norm_eq_enorm]は, EをSeminormedGroupからSeminormedAddGroupに変え, ofReal_norm_eq_enormの二項演算子*を+に変えたバージョンを生成するためのタグです.

variable [SeminormedGroup E]

@[to_additive ofReal_norm_eq_enorm]
lemma ofReal_norm_eq_enorm' (a : E) : .ofReal ‖a‖ = ‖a‖ₑ := ENNReal.ofReal_eq_coe_nnreal _