Change of measure for set-to-function extensions #
This file develops compatibility of MeasureTheory.setToFun with measurable maps and changes of
measure. It first proves approximation results using integrable simple functions, then compares
setToFun across dominated measures and establishes formulas for sums and scalar multiples of
measures.
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 α}
{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 α}
{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.setToFun_of_le_map_of_stronglyMeasurable
{α : 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)
{β : Type u_5}
{x✝ : MeasurableSpace β}
{μ' : Measure β}
{φ : α → β}
{T' : Set β → E →L[ℝ] F}
(hT' : DominatedFinMeasAdditive μ' T' C')
{f : β → E}
(hf : Integrable (f ∘ φ) μ)
(hfm : StronglyMeasurable f)
(hφ : Measurable φ)
(hμ' : μ' ≤ Measure.map φ μ)
(h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x)
:
theorem
MeasureTheory.setToFun_of_le_map
{α : 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)
{β : Type u_5}
{x✝ : MeasurableSpace β}
{μ' : Measure β}
{φ : α → β}
{T' : Set β → E →L[ℝ] F}
(hT' : DominatedFinMeasAdditive μ' T' C')
{f : β → E}
(hf : Integrable (f ∘ φ) μ)
(hfm : AEStronglyMeasurable f (Measure.map φ μ))
(hφ : Measurable φ)
(hμ' : μ' ≤ Measure.map φ μ)
(h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x)
:
theorem
MeasureTheory.continuous_L1_toL1
{α : Type u_1}
{G : Type u_4}
[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 α}
{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 α}
{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 α}
{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 α}
{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_add_measure
{α : 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' : ℝ}
{f : α → E}
{ν : Measure α}
(hTμ : DominatedFinMeasAdditive μ T C)
(hTν : DominatedFinMeasAdditive ν T' C')
(hμ : Integrable f μ)
(hν : Integrable f ν)
:
theorem
MeasureTheory.setToFun_sub_measure
{α : 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' : ℝ}
{f : α → E}
{ν : Measure α}
(hTμ : DominatedFinMeasAdditive μ T C)
(hTν : DominatedFinMeasAdditive ν T' C')
(hμ : Integrable f μ)
(hν : Integrable f ν)
:
theorem
MeasureTheory.setToFun_finsetSum_measure
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{f : α → E}
{ι : Type u_5}
{s : Finset ι}
(hs : s.Nonempty)
{μ : ι → Measure α}
{T : ι → Set α → E →L[ℝ] F}
{C : ι → ℝ}
(hTs : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i))
(hf : ∀ i ∈ s, Integrable f (μ i))
:
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 α}
{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 α}
{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.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 α}
{T : Set α → E →L[ℝ] F}
{C C' : ℝ}
(c : NNReal)
(hT : DominatedFinMeasAdditive μ T C)
(hT_smul : DominatedFinMeasAdditive (c • μ) 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 α}
{T T' T'' : Set α → E →L[ℝ] F}
{C C' C'' : ℝ}
{f : α → E}
{hT : DominatedFinMeasAdditive μ T C}
{hT' : DominatedFinMeasAdditive μ' T' C'}
{hT'' : DominatedFinMeasAdditive μ'' T'' C''}
(h : ∀ (s : Set α), MeasurableSet s → (μ + μ') s < ⊤ → T'' s = T s + T' s)
(hf : Integrable f μ)
(hf' : Integrable f μ')
(hμ : μ'' ≤ μ + μ')
(hC : 0 ≤ C)
(hC' : 0 ≤ C')
(hC'' : 0 ≤ C'')
:
setToFun applied to the sum T + T' of two operators is the sum of the corresponding
setToFun.