Extension of a linear function from indicators to L1 #
Given T : Set α → E →L[ℝ] F with DominatedFinMeasAdditive μ T C, we construct an extension
of T to integrable simple functions, which are finite sums of indicators of measurable sets
with finite measure, then to integrable functions, which are limits of integrable simple functions.
The main result is a continuous linear map (α →₁[μ] E) →L[ℝ] F.
This extension process is used to define the Bochner integral
in the Mathlib.MeasureTheory.Integral.Bochner.Basic file
and the conditional expectation of an integrable function
in Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1.
Main definitions #
setToL1 (hT : DominatedFinMeasAdditive μ T C) : (α →₁[μ] E) →L[ℝ] F: the extension ofTfrom indicators to L1.setToFun μ T (hT : DominatedFinMeasAdditive μ T C) (f : α → E) : F: a version of the extension which applies to functions (with value 0 if the function is not integrable).
Properties #
For most properties of setToFun, we provide two lemmas. One version uses hypotheses valid on
all sets, like T = T', and a second version which uses a primed name uses hypotheses on
measurable sets with finite measure, like ∀ s, MeasurableSet s → μ s < ∞ → T s = T' s.
The lemmas listed here don't show all hypotheses. Refer to the actual lemmas for details.
Linearity:
setToFun_zero_left : setToFun μ 0 hT f = 0setToFun_add_left : setToFun μ (T + T') _ f = setToFun μ T hT f + setToFun μ T' hT' fsetToFun_smul_left : setToFun μ (fun s ↦ c • (T s)) (hT.smul c) f = c • setToFun μ T hT fsetToFun_zero : setToFun μ T hT (0 : α → E) = 0setToFun_neg : setToFun μ T hT (-f) = - setToFun μ T hT fIffandgare integrable:setToFun_add : setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT gsetToFun_sub : setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT gIfTis verifies∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x:setToFun_smul : setToFun μ T hT (c • f) = c • setToFun μ T hT f
Other:
setToFun_congr_ae (h : f =ᵐ[μ] g) : setToFun μ T hT f = setToFun μ T hT gsetToFun_measure_zero (h : μ = 0) : setToFun μ T hT f = 0
If the space is a NormedLatticeAddCommGroup and T is such that 0 ≤ T s x for 0 ≤ x, we
also prove order-related properties:
setToFun_mono_left (h : ∀ s x, T s x ≤ T' s x) : setToFun μ T hT f ≤ setToFun μ T' hT' fsetToFun_nonneg (hf : 0 ≤ᵐ[μ] f) : 0 ≤ setToFun μ T hT fsetToFun_mono (hfg : f ≤ᵐ[μ] g) : setToFun μ T hT f ≤ setToFun μ T hT g
theorem
MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul
{α : Type u_1}
{G : Type u_5}
[NormedAddCommGroup G]
{m : MeasurableSpace α}
{μ : Measure α}
(f : ↥(Lp.simpleFunc G 1 μ))
:
def
MeasureTheory.L1.SimpleFunc.setToL1S
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(T : Set α → E →L[ℝ] F)
(f : ↥(Lp.simpleFunc E 1 μ))
:
F
Extend Set α → (E →L[ℝ] F') to (α →₁ₛ[μ] E) → F'.
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_eq_setToSimpleFunc
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(T : Set α → E →L[ℝ] F)
(f : ↥(Lp.simpleFunc E 1 μ))
:
@[simp]
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_zero_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_zero_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_congr
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(T : Set α → E →L[ℝ] F)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T)
{f g : ↥(Lp.simpleFunc E 1 μ)}
(h : ⇑(Lp.simpleFunc.toSimpleFunc f) =ᶠ[ae μ] ⇑(Lp.simpleFunc.toSimpleFunc g))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_congr_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(T T' : Set α → E →L[ℝ] F)
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_congr_measure
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ μ' : Measure α}
(T : Set α → E →L[ℝ] F)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T)
(hμ : μ.AbsolutelyContinuous μ')
(f : ↥(Lp.simpleFunc E 1 μ))
(f' : ↥(Lp.simpleFunc E 1 μ'))
(h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f')
:
setToL1S does not change if we replace the measure μ by μ' with μ ≪ μ'. The statement
uses two functions f and f' because they have to belong to different types, but morally these
are the same function (we have f =ᵐ[μ] f').
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_add_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(T T' : Set α → E →L[ℝ] F)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_add_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(T T' T'' : Set α → E →L[ℝ] F)
(h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_smul_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(T : Set α → E →L[ℝ] F)
(c : ℝ)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_smul_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(T T' : Set α → E →L[ℝ] F)
(c : ℝ)
(h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_add
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(T : Set α → E →L[ℝ] F)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T)
(f g : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_neg
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_sub
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T)
(f g : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_smul_real
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(T : Set α → E →L[ℝ] F)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T)
(c : ℝ)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_smul
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_6}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[NormedField 𝕜]
{E : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedSpace 𝕜 E]
[DistribSMul 𝕜 F]
(T : Set α → E →L[ℝ] F)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
(c : 𝕜)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.norm_setToL1S_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
(T : Set α → E →L[ℝ] F)
{C : ℝ}
(hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * μ.real s)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{s : Set α}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T)
(hs : MeasurableSet s)
(hμs : μ s < ⊤)
(x : E)
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_const
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
{T : Set α → E →L[ℝ] F}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T)
(x : E)
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_mono_left
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : Measure α}
{G'' : Type u_7}
[NormedAddCommGroup G'']
[Lattice G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
{T T' : Set α → E →L[ℝ] G''}
(hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_mono_left'
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : Measure α}
{G'' : Type u_7}
[NormedAddCommGroup G'']
[Lattice G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
{T T' : Set α → E →L[ℝ] G''}
(hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{G'' : Type u_7}
{G' : Type u_8}
[NormedAddCommGroup G']
[Lattice G']
[IsOrderedAddMonoid G']
[NormedSpace ℝ G']
[NormedAddCommGroup G'']
[Lattice G'']
[NormedSpace ℝ G'']
{T : Set α → G'' →L[ℝ] G'}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x)
{f : ↥(Lp.simpleFunc G'' 1 μ)}
(hf : 0 ≤ f)
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_mono
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{G'' : Type u_7}
{G' : Type u_8}
[NormedAddCommGroup G']
[Lattice G']
[IsOrderedAddMonoid G']
[NormedSpace ℝ G']
[NormedAddCommGroup G'']
[Lattice G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
{T : Set α → G'' →L[ℝ] G'}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x)
{f g : ↥(Lp.simpleFunc G'' 1 μ)}
(hfg : f ≤ g)
:
def
MeasureTheory.L1.SimpleFunc.setToL1SCLM'
(α : Type u_1)
(E : Type u_2)
{F : Type u_3}
(𝕜 : Type u_6)
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
(μ : Measure α)
[NormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
:
Extend Set α → E →L[ℝ] F to (α →₁ₛ[μ] E) →L[𝕜] F.
Equations
- MeasureTheory.L1.SimpleFunc.setToL1SCLM' α E 𝕜 μ hT h_smul = { toFun := MeasureTheory.L1.SimpleFunc.setToL1S T, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous C ⋯
def
MeasureTheory.L1.SimpleFunc.setToL1SCLM
(α : Type u_1)
(E : Type u_2)
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
(μ : Measure α)
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
:
Extend Set α → E →L[ℝ] F to (α →₁ₛ[μ] E) →L[ℝ] F.
Equations
- MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT = { toFun := MeasureTheory.L1.SimpleFunc.setToL1S T, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous C ⋯
@[simp]
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ 0 C)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T T' : Set α → E →L[ℝ] F}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(h : T = T')
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T T' : Set α → E →L[ℝ] F}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_measure
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C C' : ℝ}
{μ' : Measure α}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ' T C')
(hμ : μ.AbsolutelyContinuous μ')
(f : ↥(Lp.simpleFunc E 1 μ))
(f' : ↥(Lp.simpleFunc E 1 μ'))
(h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f')
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T T' : Set α → E →L[ℝ] F}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T T' T'' : Set α → E →L[ℝ] F}
{C C' C'' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(hT'' : DominatedFinMeasAdditive μ T'' C'')
(h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(c : ℝ)
(hT : DominatedFinMeasAdditive μ T C)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T T' : Set α → E →L[ℝ] F}
{C C' : ℝ}
(c : ℝ)
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hC : 0 ≤ C)
:
theorem
MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_const
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(x : E)
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : Measure α}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
{T T' : Set α → E →L[ℝ] G''}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left'
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : Measure α}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
{T T' : Set α → E →L[ℝ] G''}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
[NormedAddCommGroup G']
[Lattice G']
[NormedSpace ℝ G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f : ↥(Lp.simpleFunc G' 1 μ)}
(hf : 0 ≤ f)
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
[NormedAddCommGroup G']
[Lattice G']
[IsOrderedAddMonoid G']
[NormedSpace ℝ G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f g : ↥(Lp.simpleFunc G' 1 μ)}
(hfg : f ≤ g)
:
def
MeasureTheory.L1.setToL1'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
(𝕜 : Type u_6)
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
:
Extend Set α → (E →L[ℝ] F) to (α →₁[μ] E) →L[𝕜] F.
Equations
- MeasureTheory.L1.setToL1' 𝕜 hT h_smul = (MeasureTheory.L1.SimpleFunc.setToL1SCLM' α E 𝕜 μ hT h_smul).extend (MeasureTheory.Lp.simpleFunc.coeToLp α E 𝕜) ⋯ ⋯
def
MeasureTheory.L1.setToL1
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
:
Extend Set α → E →L[ℝ] F to (α →₁[μ] E) →L[ℝ] F.
Equations
- MeasureTheory.L1.setToL1 hT = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT).extend (MeasureTheory.Lp.simpleFunc.coeToLp α E ℝ) ⋯ ⋯
theorem
MeasureTheory.L1.setToL1_eq_setToL1SCLM
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(f : ↥(Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_eq_setToL1'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{𝕜 : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
(f : ↥(Lp E 1 μ))
:
@[simp]
theorem
MeasureTheory.L1.setToL1_zero_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{C : ℝ}
(hT : DominatedFinMeasAdditive μ 0 C)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_zero_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_congr_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
(T T' : Set α → E →L[ℝ] F)
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(h : T = T')
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_congr_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
(T T' : Set α → E →L[ℝ] F)
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_add_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T T' : Set α → E →L[ℝ] F}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_add_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T T' T'' : Set α → E →L[ℝ] F}
{C C' C'' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(hT'' : DominatedFinMeasAdditive μ T'' C'')
(h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_smul_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(c : ℝ)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_smul_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T T' : Set α → E →L[ℝ] F}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(c : ℝ)
(h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_smul
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{𝕜 : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
(c : 𝕜)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_simpleFunc_indicatorConst
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s < ⊤)
(x : E)
:
theorem
MeasureTheory.L1.setToL1_indicatorConstLp
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : E)
:
theorem
MeasureTheory.L1.setToL1_const
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
[IsFiniteMeasure μ]
(hT : DominatedFinMeasAdditive μ T C)
(x : E)
:
theorem
MeasureTheory.L1.setToL1_mono_left'
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : Measure α}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[HasSolidNorm G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
{T T' : Set α → E →L[ℝ] G''}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_mono_left
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : Measure α}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[HasSolidNorm G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
{T T' : Set α → E →L[ℝ] G''}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.setToL1_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[HasSolidNorm G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
[NormedAddCommGroup G']
[Lattice G']
[NormedSpace ℝ G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f : ↥(Lp G' 1 μ)}
(hf : 0 ≤ f)
:
theorem
MeasureTheory.L1.setToL1_mono
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[HasSolidNorm G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
[NormedAddCommGroup G']
[Lattice G']
[NormedSpace ℝ G']
[IsOrderedAddMonoid G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f g : ↥(Lp G' 1 μ)}
(hfg : f ≤ g)
:
theorem
MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
:
theorem
MeasureTheory.L1.norm_setToL1_le_mul_norm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hC : 0 ≤ C)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.norm_setToL1_le_mul_norm'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.L1.norm_setToL1_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hC : 0 ≤ C)
:
theorem
MeasureTheory.L1.norm_setToL1_le'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
:
theorem
MeasureTheory.L1.setToL1_lipschitz
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
:
LipschitzWith C.toNNReal ⇑(setToL1 hT)
theorem
MeasureTheory.L1.tendsto_setToL1
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(f : ↥(Lp E 1 μ))
{ι : Type u_7}
(fs : ι → ↥(Lp E 1 μ))
{l : Filter ι}
(hfs : Filter.Tendsto fs l (nhds f))
:
Filter.Tendsto (fun (i : ι) => (setToL1 hT) (fs i)) l (nhds ((setToL1 hT) f))
def
MeasureTheory.setToFun
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
(μ : Measure α)
[CompleteSpace F]
(T : Set α → E →L[ℝ] F)
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(f : α → E)
:
F
Extend T : Set α → E →L[ℝ] F to (α → E) → F (for integrable functions α → E). We set it to
0 if the function is not integrable.
Equations
- MeasureTheory.setToFun μ T hT f = if hf : MeasureTheory.Integrable f μ then (MeasureTheory.L1.setToL1 hT) (MeasureTheory.Integrable.toL1 f hf) else 0
theorem
MeasureTheory.setToFun_eq
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hf : Integrable f μ)
:
theorem
MeasureTheory.L1.setToFun_eq_setToL1
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.setToFun_undef
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hf : ¬Integrable f μ)
:
theorem
MeasureTheory.setToFun_non_aestronglyMeasurable
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hf : ¬AEStronglyMeasurable f μ)
:
@[deprecated MeasureTheory.setToFun_non_aestronglyMeasurable (since := "2025-04-09")]
theorem
MeasureTheory.setToFun_non_aEStronglyMeasurable
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hf : ¬AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.setToFun_congr_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T T' : Set α → E →L[ℝ] F}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(h : T = T')
(f : α → E)
:
theorem
MeasureTheory.setToFun_congr_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T T' : Set α → E →L[ℝ] F}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s)
(f : α → E)
:
theorem
MeasureTheory.setToFun_add_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T T' : Set α → E →L[ℝ] F}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(f : α → E)
:
theorem
MeasureTheory.setToFun_add_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T T' T'' : Set α → E →L[ℝ] F}
{C C' C'' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(hT'' : DominatedFinMeasAdditive μ T'' C'')
(h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s)
(f : α → E)
:
theorem
MeasureTheory.setToFun_smul_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(c : ℝ)
(f : α → E)
:
theorem
MeasureTheory.setToFun_smul_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T T' : Set α → E →L[ℝ] F}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(c : ℝ)
(h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s)
(f : α → E)
:
@[simp]
theorem
MeasureTheory.setToFun_zero
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
:
@[simp]
theorem
MeasureTheory.setToFun_zero_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{C : ℝ}
{f : α → E}
{hT : DominatedFinMeasAdditive μ 0 C}
:
theorem
MeasureTheory.setToFun_zero_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0)
:
theorem
MeasureTheory.setToFun_add
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f g : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hf : Integrable f μ)
(hg : Integrable g μ)
:
theorem
MeasureTheory.setToFun_finset_sum'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{ι : Type u_7}
(s : Finset ι)
{f : ι → α → E}
(hf : ∀ i ∈ s, Integrable (f i) μ)
:
theorem
MeasureTheory.setToFun_finset_sum
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{ι : Type u_7}
(s : Finset ι)
{f : ι → α → E}
(hf : ∀ i ∈ s, Integrable (f i) μ)
:
theorem
MeasureTheory.setToFun_neg
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(f : α → E)
:
theorem
MeasureTheory.setToFun_sub
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f g : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hf : Integrable f μ)
(hg : Integrable g μ)
:
theorem
MeasureTheory.setToFun_smul
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{𝕜 : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
(hT : DominatedFinMeasAdditive μ T C)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
(c : 𝕜)
(f : α → E)
:
theorem
MeasureTheory.setToFun_congr_ae
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f g : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(h : f =ᶠ[ae μ] g)
:
theorem
MeasureTheory.setToFun_measure_zero
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(h : μ = 0)
:
theorem
MeasureTheory.setToFun_measure_zero'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → μ s = 0)
:
theorem
MeasureTheory.setToFun_toL1
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hf : Integrable f μ)
:
theorem
MeasureTheory.setToFun_indicator_const
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : E)
:
theorem
MeasureTheory.setToFun_const
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
[IsFiniteMeasure μ]
(hT : DominatedFinMeasAdditive μ T C)
(x : E)
:
theorem
MeasureTheory.setToFun_mono_left'
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : Measure α}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[HasSolidNorm G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
{T T' : Set α → E →L[ℝ] G''}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x)
(f : α → E)
:
theorem
MeasureTheory.setToFun_mono_left
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : Measure α}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[HasSolidNorm G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
{T T' : Set α → E →L[ℝ] G''}
{C C' : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.setToFun_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[HasSolidNorm G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
[NormedAddCommGroup G']
[Lattice G']
[NormedSpace ℝ G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f : α → G'}
(hf : 0 ≤ᶠ[ae μ] f)
:
theorem
MeasureTheory.setToFun_mono
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedAddCommGroup G'']
[Lattice G'']
[HasSolidNorm G'']
[IsOrderedAddMonoid G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
[NormedAddCommGroup G']
[Lattice G']
[NormedSpace ℝ G']
[IsOrderedAddMonoid G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f g : α → G'}
(hf : Integrable f μ)
(hg : Integrable g μ)
(hfg : f ≤ᶠ[ae μ] g)
:
theorem
MeasureTheory.continuous_setToFun
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
:
Continuous fun (f : ↥(Lp E 1 μ)) => setToFun μ T hT ↑↑f
theorem
MeasureTheory.tendsto_setToFun_of_L1
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{ι : Type u_7}
(f : α → E)
(hfi : Integrable f μ)
{fs : ι → α → E}
{l : Filter ι}
(hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ)
(hfs : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (nhds 0))
:
Filter.Tendsto (fun (i : ι) => setToFun μ T hT (fs i)) l (nhds (setToFun μ T hT f))
If F i → f in L1, then setToFun μ T hT (F i) → setToFun μ T hT f.
theorem
MeasureTheory.tendsto_setToFun_approxOn_of_measurable
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
[MeasurableSpace E]
[BorelSpace E]
{f : α → E}
{s : Set E}
[TopologicalSpace.SeparableSpace ↑s]
(hfi : Integrable f μ)
(hfm : Measurable f)
(hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s)
{y₀ : E}
(h₀ : y₀ ∈ s)
(h₀i : Integrable (fun (x : α) => y₀) μ)
:
Filter.Tendsto (fun (n : ℕ) => setToFun μ T hT ⇑(SimpleFunc.approxOn f hfm s y₀ h₀ n)) Filter.atTop
(nhds (setToFun μ T hT f))
theorem
MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
[MeasurableSpace E]
[BorelSpace E]
{f : α → E}
(fmeas : Measurable f)
(hf : Integrable f μ)
(s : Set E)
[TopologicalSpace.SeparableSpace ↑s]
(hs : Set.range f ∪ {0} ⊆ s)
:
Filter.Tendsto (fun (n : ℕ) => setToFun μ T hT ⇑(SimpleFunc.approxOn f fmeas s 0 ⋯ n)) Filter.atTop
(nhds (setToFun μ T hT f))
theorem
MeasureTheory.continuous_L1_toL1
{α : Type u_1}
{G : Type u_5}
[NormedAddCommGroup G]
{m : MeasurableSpace α}
{μ μ' : Measure α}
(c' : ENNReal)
(hc' : c' ≠ ⊤)
(hμ'_le : μ' ≤ c' • μ)
:
Continuous fun (f : ↥(Lp G 1 μ)) => Integrable.toL1 ↑↑f ⋯
Auxiliary lemma for setToFun_congr_measure: the function sending f : α →₁[μ] G to
f : α →₁[μ'] G is continuous when μ' ≤ c' • μ for c' ≠ ∞.
theorem
MeasureTheory.setToFun_congr_measure_of_integrable
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C C' : ℝ}
{μ' : Measure α}
(c' : ENNReal)
(hc' : c' ≠ ⊤)
(hμ'_le : μ' ≤ c' • μ)
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ' T C')
(f : α → E)
(hfμ : Integrable f μ)
:
theorem
MeasureTheory.setToFun_congr_measure
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C C' : ℝ}
{μ' : Measure α}
(c c' : ENNReal)
(hc : c ≠ ⊤)
(hc' : c' ≠ ⊤)
(hμ_le : μ ≤ c • μ')
(hμ'_le : μ' ≤ c' • μ)
(hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ' T C')
(f : α → E)
:
theorem
MeasureTheory.setToFun_congr_measure_of_add_right
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C C' : ℝ}
{μ' : Measure α}
(hT_add : DominatedFinMeasAdditive (μ + μ') T C')
(hT : DominatedFinMeasAdditive μ T C)
(f : α → E)
(hf : Integrable f (μ + μ'))
:
theorem
MeasureTheory.setToFun_congr_measure_of_add_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C C' : ℝ}
{μ' : Measure α}
(hT_add : DominatedFinMeasAdditive (μ + μ') T C')
(hT : DominatedFinMeasAdditive μ' T C)
(f : α → E)
(hf : Integrable f (μ + μ'))
:
theorem
MeasureTheory.setToFun_top_smul_measure
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive (⊤ • μ) T C)
(f : α → E)
:
theorem
MeasureTheory.setToFun_congr_smul_measure
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C C' : ℝ}
(c : ENNReal)
(hc_ne_top : c ≠ ⊤)
(hT : DominatedFinMeasAdditive μ T C)
(hT_smul : DominatedFinMeasAdditive (c • μ) T C')
(f : α → E)
:
theorem
MeasureTheory.norm_setToFun_le_mul_norm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(f : ↥(Lp E 1 μ))
(hC : 0 ≤ C)
:
theorem
MeasureTheory.norm_setToFun_le_mul_norm'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
(f : ↥(Lp E 1 μ))
:
theorem
MeasureTheory.norm_setToFun_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hf : Integrable f μ)
(hC : 0 ≤ C)
:
theorem
MeasureTheory.norm_setToFun_le'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : DominatedFinMeasAdditive μ T C)
(hf : Integrable f μ)
:
theorem
MeasureTheory.tendsto_setToFun_of_dominated_convergence
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{fs : ℕ → α → E}
{f : α → E}
(bound : α → ℝ)
(fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ)
(bound_integrable : Integrable bound μ)
(h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a)
(h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => fs n a) Filter.atTop (nhds (f a)))
:
Filter.Tendsto (fun (n : ℕ) => setToFun μ T hT (fs n)) Filter.atTop (nhds (setToFun μ T hT f))
Lebesgue dominated convergence theorem provides sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their image by
setToFun.
We could weaken the condition bound_integrable to require HasFiniteIntegral bound μ instead
(i.e. not requiring that bound is measurable), but in all applications proving integrability
is easier.
theorem
MeasureTheory.tendsto_setToFun_filter_of_dominated_convergence
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : DominatedFinMeasAdditive μ T C)
{ι : Type u_7}
{l : Filter ι}
[l.IsCountablyGenerated]
{fs : ι → α → E}
{f : α → E}
(bound : α → ℝ)
(hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ)
(h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a)
(bound_integrable : Integrable bound μ)
(h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ι) => fs n a) l (nhds (f a)))
:
Filter.Tendsto (fun (n : ι) => setToFun μ T hT (fs n)) l (nhds (setToFun μ T hT f))
Lebesgue dominated convergence theorem for filters with a countable basis
theorem
MeasureTheory.continuousWithinAt_setToFun_of_dominated
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_7}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{x₀ : X}
{bound : α → ℝ}
{s : Set X}
(hfs_meas : ∀ᶠ (x : X) in nhdsWithin x₀ s, AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun (x : X) => fs x a) s x₀)
:
ContinuousWithinAt (fun (x : X) => setToFun μ T hT (fs x)) s x₀
theorem
MeasureTheory.continuousAt_setToFun_of_dominated
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_7}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{x₀ : X}
{bound : α → ℝ}
(hfs_meas : ∀ᶠ (x : X) in nhds x₀, AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun (x : X) => fs x a) x₀)
:
ContinuousAt (fun (x : X) => setToFun μ T hT (fs x)) x₀
theorem
MeasureTheory.continuousOn_setToFun_of_dominated
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_7}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{bound : α → ℝ}
{s : Set X}
(hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun (x : X) => fs x a) s)
:
ContinuousOn (fun (x : X) => setToFun μ T hT (fs x)) s
theorem
MeasureTheory.continuous_setToFun_of_dominated
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_7}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{bound : α → ℝ}
(hfs_meas : ∀ (x : X), AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, Continuous fun (x : X) => fs x a)
:
Continuous fun (x : X) => setToFun μ T hT (fs x)