Integrable functions and L¹ space
In the first part of this file, the predicate integrable is defined and basic properties of
integrable functions are proved.
In the second part, the space L¹ of equivalence classes of integrable functions under the relation
of being almost everywhere equal is defined as a subspace of the space L⁰. See the file
src/measure_theory/ae_eq_fun.lean for information on L⁰ space.
Notation
α →₁ βis the type ofL¹space, whereαis ameasure_spaceandβis anormed_groupwith asecond_countable_topology.f : α →ₘ βis a "function" inL¹. In comments,[f]is also used to denote anL¹function.₁can be typed as\1.
Main definitions
Let
f : α → βbe a function, whereαis ameasure_spaceandβanormed_group. Thenfis calledintegrableif(∫⁻ a, nnnorm (f a)) < ⊤holds.The space
L¹is defined as a subspace ofL⁰: Anae_eq_fun[f] : α →ₘ βis in the spaceL¹ifedist [f] 0 < ⊤, which means(∫⁻ a, edist (f a) 0) < ⊤if we expand the definition ofedistinL⁰.
Main statements
L¹, as a subspace, inherits most of the structures of L⁰.
Implementation notes
Maybe integrable f should be mean (∫⁻ a, edist (f a) 0) < ⊤, so that integrable and
ae_eq_fun.integrable are more aligned. But in the end one can use the lemma
lintegral_nnnorm_eq_lintegral_edist : (∫⁻ a, nnnorm (f a)) = (∫⁻ a, edist (f a) 0) to switch the
two forms.
Tags
integrable, function space, l1
def
measure_theory.integrable
{α : Type u}
[measurable_space α]
{β : Type v}
[normed_group β] :
(α → β) → (measure_theory.measure α . "volume_tac") → Prop
integrable f μ means that the integral ∫⁻ a, ∥f a∥ ∂μ is finite; integrable f means
integrable f volume.
theorem
measure_theory.integrable_iff_norm
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
(f : α → β) :
measure_theory.integrable f μ ↔ ∫⁻ (a : α), ennreal.of_real ∥f a∥ ∂μ < ⊤
theorem
measure_theory.integrable_iff_edist
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
(f : α → β) :
measure_theory.integrable f μ ↔ ∫⁻ (a : α), has_edist.edist (f a) 0 ∂μ < ⊤
theorem
measure_theory.integrable_iff_of_real
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ℝ} :
0 ≤ᵐ[μ] f → (measure_theory.integrable f μ ↔ ∫⁻ (a : α), ennreal.of_real (f a) ∂μ < ⊤)
theorem
measure_theory.integrable.mono
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{γ : Type w}
[normed_group γ]
{f : α → β}
{g : α → γ} :
measure_theory.integrable g μ → (∀ᵐ (a : α) ∂μ, ∥f a∥ ≤ ∥g a∥) → measure_theory.integrable f μ
theorem
measure_theory.integrable.mono'
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f : α → β}
{g : α → ℝ} :
measure_theory.integrable g μ → (∀ᵐ (a : α) ∂μ, ∥f a∥ ≤ g a) → measure_theory.integrable f μ
theorem
measure_theory.integrable.congr'
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{γ : Type w}
[normed_group γ]
{f : α → β}
{g : α → γ} :
measure_theory.integrable f μ → (∀ᵐ (a : α) ∂μ, ∥f a∥ = ∥g a∥) → measure_theory.integrable g μ
theorem
measure_theory.integrable_congr'
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{γ : Type w}
[normed_group γ]
{f : α → β}
{g : α → γ} :
(∀ᵐ (a : α) ∂μ, ∥f a∥ = ∥g a∥) → (measure_theory.integrable f μ ↔ measure_theory.integrable g μ)
theorem
measure_theory.integrable.congr
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f g : α → β} :
measure_theory.integrable f μ → f =ᵐ[μ] g → measure_theory.integrable g μ
theorem
measure_theory.integrable_congr
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f g : α → β} :
f =ᵐ[μ] g → (measure_theory.integrable f μ ↔ measure_theory.integrable g μ)
theorem
measure_theory.integrable_const_iff
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{c : β} :
theorem
measure_theory.integrable_const
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[measure_theory.finite_measure μ]
(c : β) :
measure_theory.integrable (λ (x : α), c) μ
theorem
measure_theory.integrable_of_bounded
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[measure_theory.finite_measure μ]
{f : α → β}
{C : ℝ} :
(∀ᵐ (a : α) ∂μ, ∥f a∥ ≤ C) → measure_theory.integrable f μ
theorem
measure_theory.integrable.mono_measure
{α : Type u}
[measurable_space α]
{μ ν : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f : α → β} :
measure_theory.integrable f ν → μ ≤ ν → measure_theory.integrable f μ
theorem
measure_theory.integrable.add_measure
{α : Type u}
[measurable_space α]
{μ ν : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f : α → β} :
measure_theory.integrable f μ → measure_theory.integrable f ν → measure_theory.integrable f (μ + ν)
theorem
measure_theory.integrable.left_of_add_measure
{α : Type u}
[measurable_space α]
{μ ν : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f : α → β} :
measure_theory.integrable f (μ + ν) → measure_theory.integrable f μ
theorem
measure_theory.integrable.right_of_add_measure
{α : Type u}
[measurable_space α]
{μ ν : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f : α → β} :
measure_theory.integrable f (μ + ν) → measure_theory.integrable f ν
@[simp]
theorem
measure_theory.integrable_add_measure
{α : Type u}
[measurable_space α]
{μ ν : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f : α → β} :
measure_theory.integrable f (μ + ν) ↔ measure_theory.integrable f μ ∧ measure_theory.integrable f ν
theorem
measure_theory.integrable.smul_measure
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f : α → β}
(h : measure_theory.integrable f μ)
{c : ennreal} :
c < ⊤ → measure_theory.integrable f (c • μ)
@[simp]
theorem
measure_theory.integrable_zero_measure
{α : Type u}
[measurable_space α]
{β : Type v}
[normed_group β]
(f : α → β) :
theorem
measure_theory.integrable_map_measure
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{δ : Type u_1}
[measurable_space δ]
[measurable_space β]
[opens_measurable_space β]
{f : α → δ}
{g : δ → β} :
measurable f → measurable g → (measure_theory.integrable g (⇑(measure_theory.measure.map f) μ) ↔ measure_theory.integrable (g ∘ f) μ)
theorem
measure_theory.lintegral_nnnorm_eq_lintegral_edist
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
(f : α → β) :
theorem
measure_theory.lintegral_norm_eq_lintegral_edist
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
(f : α → β) :
theorem
measure_theory.lintegral_edist_triangle
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β]
{f g h : α → β} :
measurable f → measurable g → measurable h → ∫⁻ (a : α), has_edist.edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), has_edist.edist (f a) (h a) ∂μ + ∫⁻ (a : α), has_edist.edist (g a) (h a) ∂μ
theorem
measure_theory.lintegral_edist_lt_top
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β]
{f g : α → β} :
measurable f → measure_theory.integrable f μ → measurable g → measure_theory.integrable g μ → ∫⁻ (a : α), has_edist.edist (f a) (g a) ∂μ < ⊤
theorem
measure_theory.lintegral_nnnorm_zero
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β] :
@[simp]
theorem
measure_theory.integrable_zero
(α : Type u)
[measurable_space α]
(μ : measure_theory.measure α)
(β : Type v)
[normed_group β] :
measure_theory.integrable (λ (a : α), 0) μ
theorem
measure_theory.lintegral_nnnorm_add
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{γ : Type w}
[normed_group γ]
[measurable_space β]
[opens_measurable_space β]
[measurable_space γ]
[opens_measurable_space γ]
{f : α → β}
{g : α → γ} :
theorem
measure_theory.integrable.add
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[measurable_space β]
[opens_measurable_space β]
{f g : α → β} :
measurable f → measure_theory.integrable f μ → measurable g → measure_theory.integrable g μ → measure_theory.integrable (f + g) μ
theorem
measure_theory.integrable_finset_sum
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{ι : Type u_1}
[measurable_space β]
[borel_space β]
[topological_space.second_countable_topology β]
(s : finset ι)
{f : ι → α → β} :
(∀ (i : ι), measurable (f i)) → (∀ (i : ι), measure_theory.integrable (f i) μ) → measure_theory.integrable (λ (a : α), s.sum (λ (i : ι), f i a)) μ
theorem
measure_theory.lintegral_nnnorm_neg
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f : α → β} :
theorem
measure_theory.integrable.neg
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f : α → β} :
measure_theory.integrable f μ → measure_theory.integrable (-f) μ
@[simp]
theorem
measure_theory.integrable_neg_iff
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f : α → β} :
theorem
measure_theory.integrable.sub
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[measurable_space β]
[opens_measurable_space β]
{f g : α → β} :
measurable f → measure_theory.integrable f μ → measurable g → measure_theory.integrable g μ → measure_theory.integrable (f - g) μ
theorem
measure_theory.integrable.norm
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{f : α → β} :
measure_theory.integrable f μ → measure_theory.integrable (λ (a : α), ∥f a∥) μ
theorem
measure_theory.integrable_norm_iff
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
(f : α → β) :
measure_theory.integrable (λ (a : α), ∥f a∥) μ ↔ measure_theory.integrable f μ
theorem
measure_theory.all_ae_of_real_F_le_bound
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{F : ℕ → α → β}
{bound : α → ℝ}
(h : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ∥F n a∥ ≤ bound a)
(n : ℕ) :
∀ᵐ (a : α) ∂μ, ennreal.of_real ∥F n a∥ ≤ ennreal.of_real (bound a)
theorem
measure_theory.all_ae_tendsto_of_real_norm
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{F : ℕ → α → β}
{f : α → β} :
(∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ℕ), F n a) filter.at_top (nhds (f a))) → (∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ℕ), ennreal.of_real ∥F n a∥) filter.at_top (nhds (ennreal.of_real ∥f a∥)))
theorem
measure_theory.all_ae_of_real_f_le_bound
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{F : ℕ → α → β}
{f : α → β}
{bound : α → ℝ} :
(∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ∥F n a∥ ≤ bound a) → (∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ℕ), F n a) filter.at_top (nhds (f a))) → (∀ᵐ (a : α) ∂μ, ennreal.of_real ∥f a∥ ≤ ennreal.of_real (bound a))
theorem
measure_theory.integrable_of_dominated_convergence
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{F : ℕ → α → β}
{f : α → β}
{bound : α → ℝ} :
measure_theory.integrable bound μ → (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ∥F n a∥ ≤ bound a) → (∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ℕ), F n a) filter.at_top (nhds (f a))) → measure_theory.integrable f μ
theorem
measure_theory.tendsto_lintegral_norm_of_dominated_convergence
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[measurable_space β]
[borel_space β]
[topological_space.second_countable_topology β]
{F : ℕ → α → β}
{f : α → β}
{bound : α → ℝ} :
(∀ (n : ℕ), measurable (F n)) → measurable f → measure_theory.integrable bound μ → (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ∥F n a∥ ≤ bound a) → (∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ℕ), F n a) filter.at_top (nhds (f a))) → filter.tendsto (λ (n : ℕ), ∫⁻ (a : α), ennreal.of_real ∥F n a - f a∥ ∂μ) filter.at_top (nhds 0)
Lemmas used for defining the positive part of a L¹ function
theorem
measure_theory.integrable.max_zero
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ℝ} :
measure_theory.integrable f μ → measure_theory.integrable (λ (a : α), max (f a) 0) μ
theorem
measure_theory.integrable.min_zero
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ℝ} :
measure_theory.integrable f μ → measure_theory.integrable (λ (a : α), min (f a) 0) μ
theorem
measure_theory.integrable.smul
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{𝕜 : Type u_1}
[normed_field 𝕜]
[normed_space 𝕜 β]
(c : 𝕜)
{f : α → β} :
measure_theory.integrable f μ → measure_theory.integrable (c • f) μ
theorem
measure_theory.integrable_smul_iff
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
{𝕜 : Type u_1}
[normed_field 𝕜]
[normed_space 𝕜 β]
{c : 𝕜}
(hc : c ≠ 0)
(f : α → β) :
measure_theory.integrable (c • f) μ ↔ measure_theory.integrable f μ
def
measure_theory.ae_eq_fun.integrable
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β] :
An almost everywhere equal function is integrable if it has a finite distance to the origin.
Should mean the same thing as the predicate integrable over functions.
Equations
- f.integrable = (f ∈ emetric.ball 0 ⊤)
theorem
measure_theory.ae_eq_fun.integrable_mk
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β]
{f : α → β}
(hf : measurable f) :
theorem
measure_theory.ae_eq_fun.integrable_coe_fn
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β]
{f : α →ₘ[μ] β} :
theorem
measure_theory.ae_eq_fun.integrable_zero
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β] :
theorem
measure_theory.ae_eq_fun.integrable.add
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{f g : α →ₘ[μ] β} :
f.integrable → g.integrable → (f + g).integrable
theorem
measure_theory.ae_eq_fun.integrable.neg
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{f : α →ₘ[μ] β} :
f.integrable → (-f).integrable
theorem
measure_theory.ae_eq_fun.integrable.sub
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{f g : α →ₘ[μ] β} :
f.integrable → g.integrable → (f - g).integrable
theorem
measure_theory.ae_eq_fun.is_add_subgroup
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β] :
theorem
measure_theory.ae_eq_fun.integrable.smul
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{𝕜 : Type u_1}
[normed_field 𝕜]
[normed_space 𝕜 β]
{c : 𝕜}
{f : α →ₘ[μ] β} :
f.integrable → (c • f).integrable
def
measure_theory.l1
(α : Type u)
[measurable_space α]
(β : Type v)
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β] :
measure_theory.measure α → Type (max u v)
The space of equivalence classes of integrable (and measurable) functions, where two integrable
functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure
0.
Equations
- (α →₁[μ] β) = {f // f.integrable}
@[instance]
def
measure_theory.l1.has_coe
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β] :
Equations
@[instance]
def
measure_theory.l1.has_coe_to_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β] :
has_coe_to_fun (α →₁[μ] β)
@[simp]
theorem
measure_theory.l1.coe_coe
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β]
(f : α →₁[μ] β) :
theorem
measure_theory.l1.eq
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β]
{f g : α →₁[μ] β} :
theorem
measure_theory.l1.eq_iff
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β]
{f g : α →₁[μ] β} :
@[instance]
def
measure_theory.l1.emetric_space
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β] :
emetric_space (α →₁[μ] β)
L¹ space forms a emetric_space, with the emetric being inherited from almost everywhere
functions, i.e., edist f g = ∫⁻ a, edist (f a) (g a).
@[instance]
def
measure_theory.l1.metric_space
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[opens_measurable_space β] :
metric_space (α →₁[μ] β)
L¹ space forms a metric_space, with the metric being inherited from almost everywhere
functions, i.e., edist f g = ennreal.to_real (∫⁻ a, edist (f a) (g a)).
Equations
@[instance]
def
measure_theory.l1.add_comm_group
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β] :
add_comm_group (α →₁[μ] β)
@[instance]
def
measure_theory.l1.inhabited
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β] :
Equations
@[simp]
theorem
measure_theory.l1.coe_zero
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β] :
@[simp]
theorem
measure_theory.l1.coe_add
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f g : α →₁[μ] β) :
@[simp]
theorem
measure_theory.l1.coe_neg
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α →₁[μ] β) :
@[simp]
theorem
measure_theory.l1.coe_sub
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f g : α →₁[μ] β) :
@[simp]
theorem
measure_theory.l1.edist_eq
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f g : α →₁[μ] β) :
has_edist.edist f g = has_edist.edist ↑f ↑g
theorem
measure_theory.l1.dist_eq
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f g : α →₁[μ] β) :
has_dist.dist f g = (has_edist.edist ↑f ↑g).to_real
@[instance]
def
measure_theory.l1.has_norm
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β] :
The norm on L¹ space is defined to be ∥f∥ = ∫⁻ a, edist (f a) 0.
Equations
- measure_theory.l1.has_norm = {norm := λ (f : α →₁[μ] β), has_dist.dist f 0}
theorem
measure_theory.l1.norm_eq
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α →₁[μ] β) :
@[instance]
def
measure_theory.l1.normed_group
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β] :
normed_group (α →₁[μ] β)
Equations
- measure_theory.l1.normed_group = normed_group.of_add_dist measure_theory.l1.normed_group._proof_4 measure_theory.l1.normed_group._proof_5
@[instance]
def
measure_theory.l1.has_scalar
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{𝕜 : Type u_1}
[normed_field 𝕜]
[normed_space 𝕜 β] :
has_scalar 𝕜 (α →₁[μ] β)
@[simp]
theorem
measure_theory.l1.coe_smul
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{𝕜 : Type u_1}
[normed_field 𝕜]
[normed_space 𝕜 β]
(c : 𝕜)
(f : α →₁[μ] β) :
@[instance]
def
measure_theory.l1.semimodule
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{𝕜 : Type u_1}
[normed_field 𝕜]
[normed_space 𝕜 β] :
semimodule 𝕜 (α →₁[μ] β)
Equations
- measure_theory.l1.semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := measure_theory.l1.has_scalar _inst_8, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[instance]
def
measure_theory.l1.normed_space
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{𝕜 : Type u_1}
[normed_field 𝕜]
[normed_space 𝕜 β] :
normed_space 𝕜 (α →₁[μ] β)
Equations
- measure_theory.l1.normed_space = {to_semimodule := measure_theory.l1.semimodule _inst_8, norm_smul_le := _}
def
measure_theory.l1.of_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α → β) :
measurable f → measure_theory.integrable f μ → (α →₁[μ] β)
Construct the equivalence class [f] of a measurable and integrable function f.
Equations
- measure_theory.l1.of_fun f hfm hfi = ⟨measure_theory.ae_eq_fun.mk f hfm, _⟩
@[simp]
theorem
measure_theory.l1.of_fun_eq_mk
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α → β)
(hfm : measurable f)
(hfi : measure_theory.integrable f μ) :
↑(measure_theory.l1.of_fun f hfm hfi) = measure_theory.ae_eq_fun.mk f hfm
theorem
measure_theory.l1.of_fun_eq_of_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f g : α → β)
(hfm : measurable f)
(hfi : measure_theory.integrable f μ)
(hgm : measurable g)
(hgi : measure_theory.integrable g μ) :
measure_theory.l1.of_fun f hfm hfi = measure_theory.l1.of_fun g hgm hgi ↔ f =ᵐ[μ] g
theorem
measure_theory.l1.of_fun_zero
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β] :
measure_theory.l1.of_fun (λ (_x : α), 0) measurable_zero _ = 0
theorem
measure_theory.l1.of_fun_add
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f g : α → β)
(hfm : measurable (λ (i : α), f i))
(hfi : measure_theory.integrable f μ)
(hgm : measurable (λ (i : α), g i))
(hgi : measure_theory.integrable g μ) :
measure_theory.l1.of_fun (f + g) _ _ = measure_theory.l1.of_fun f hfm hfi + measure_theory.l1.of_fun g hgm hgi
theorem
measure_theory.l1.of_fun_neg
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α → β)
(hfm : measurable (λ (i : α), f i))
(hfi : measure_theory.integrable f μ) :
measure_theory.l1.of_fun (-f) _ _ = -measure_theory.l1.of_fun f hfm hfi
theorem
measure_theory.l1.of_fun_sub
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f g : α → β)
(hfm : measurable (λ (i : α), f i))
(hfi : measure_theory.integrable f μ)
(hgm : measurable (λ (i : α), g i))
(hgi : measure_theory.integrable g μ) :
measure_theory.l1.of_fun (f - g) _ _ = measure_theory.l1.of_fun f hfm hfi - measure_theory.l1.of_fun g hgm hgi
theorem
measure_theory.l1.norm_of_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α → β)
(hfm : measurable f)
(hfi : measure_theory.integrable f μ) :
∥measure_theory.l1.of_fun f hfm hfi∥ = (∫⁻ (a : α), has_edist.edist (f a) 0 ∂μ).to_real
theorem
measure_theory.l1.norm_of_fun_eq_lintegral_norm
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α → β)
(hfm : measurable f)
(hfi : measure_theory.integrable f μ) :
theorem
measure_theory.l1.of_fun_smul
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{𝕜 : Type u_1}
[normed_field 𝕜]
[normed_space 𝕜 β]
(f : α → β)
(hfm : measurable f)
(hfi : measure_theory.integrable f μ)
(k : 𝕜) :
measure_theory.l1.of_fun (λ (a : α), k • f a) _ _ = k • measure_theory.l1.of_fun f hfm hfi
theorem
measure_theory.l1.measurable
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α →₁[μ] β) :
theorem
measure_theory.l1.integrable
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α →₁[μ] β) :
theorem
measure_theory.l1.of_fun_to_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α →₁[μ] β) :
measure_theory.l1.of_fun ⇑f _ _ = f
theorem
measure_theory.l1.mk_to_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α →₁[μ] β) :
theorem
measure_theory.l1.to_fun_of_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α → β)
(hfm : measurable f)
(hfi : measure_theory.integrable f μ) :
⇑(measure_theory.l1.of_fun f hfm hfi) =ᵐ[μ] f
theorem
measure_theory.l1.zero_to_fun
(α : Type u)
[measurable_space α]
{μ : measure_theory.measure α}
(β : Type v)
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β] :
theorem
measure_theory.l1.add_to_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f g : α →₁[μ] β) :
theorem
measure_theory.l1.neg_to_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α →₁[μ] β) :
theorem
measure_theory.l1.sub_to_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f g : α →₁[μ] β) :
theorem
measure_theory.l1.dist_to_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f g : α →₁[μ] β) :
has_dist.dist f g = (∫⁻ (x : α), has_edist.edist (⇑f x) (⇑g x) ∂μ).to_real
theorem
measure_theory.l1.norm_eq_nnnorm_to_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α →₁[μ] β) :
theorem
measure_theory.l1.norm_eq_norm_to_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f : α →₁[μ] β) :
theorem
measure_theory.l1.lintegral_edist_to_fun_lt_top
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
(f g : α →₁[μ] β) :
theorem
measure_theory.l1.smul_to_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{𝕜 : Type u_1}
[normed_field 𝕜]
[normed_space 𝕜 β]
(c : 𝕜)
(f : α →₁[μ] β) :
Positive part of a function in L¹ space.
Negative part of a function in L¹ space.
theorem
measure_theory.l1.coe_pos_part
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →₁[μ] ℝ) :
theorem
measure_theory.l1.pos_part_to_fun
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →₁[μ] ℝ) :
theorem
measure_theory.l1.neg_part_to_fun_eq_max
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →₁[μ] ℝ) :
theorem
measure_theory.l1.neg_part_to_fun_eq_min
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →₁[μ] ℝ) :
theorem
measure_theory.l1.norm_le_norm_of_ae_le
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type v}
[normed_group β]
[topological_space.second_countable_topology β]
[measurable_space β]
[borel_space β]
{f g : α →₁[μ] β} :
theorem
measure_theory.l1.continuous_pos_part
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α} :
continuous (λ (f : α →₁[μ] ℝ), f.pos_part)
theorem
measure_theory.l1.continuous_neg_part
{α : Type u}
[measurable_space α]
{μ : measure_theory.measure α} :
continuous (λ (f : α →₁[μ] ℝ), f.neg_part)