Extension of a linear function from indicators to L1 #
Let T : Set α → E →L[ℝ] F be additive for measurable sets with finite measure, in the sense that
for s, t two such sets, s ∩ t = ∅ → T (s ∪ t) = T s + T t. T is akin to a bilinear map on
Set α × E, or a linear map on indicator functions.
This file constructs 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 MeasureTheory.Integral.Bochner file and the conditional
expectation of an integrable function in MeasureTheory.Function.ConditionalExpectation.
Main Definitions #
FinMeasAdditive μ T: the property thatTis additive on measurable sets with finite measure. For two such sets,s ∩ t = ∅ → T (s ∪ t) = T s + T t.DominatedFinMeasAdditive μ T C:FinMeasAdditive μ T ∧ ∀ s, ‖T s‖ ≤ C * (μ s).toReal. This is the property needed to perform the extension from indicators to L1.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
Implementation notes #
The starting object T : Set α → E →L[ℝ] F matters only through its restriction on measurable sets
with finite measure. Its value on other sets is ignored.
def
MeasureTheory.FinMeasAdditive
{α : Type u_1}
{β : Type u_7}
[AddMonoid β]
:
{x : MeasurableSpace α} → MeasureTheory.Measure α → (Set α → β) → Prop
A set function is FinMeasAdditive if its value on the union of two disjoint measurable
sets with finite measure is the sum of its values on each set.
Equations
- MeasureTheory.FinMeasAdditive μ T = ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → μ s ≠ ⊤ → μ t ≠ ⊤ → s ∩ t = ∅ → T (s ∪ t) = T s + T t
Instances For
theorem
MeasureTheory.FinMeasAdditive.zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[AddCommMonoid β]
:
theorem
MeasureTheory.FinMeasAdditive.add
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[AddCommMonoid β]
{T : Set α → β}
{T' : Set α → β}
(hT : MeasureTheory.FinMeasAdditive μ T)
(hT' : MeasureTheory.FinMeasAdditive μ T')
:
MeasureTheory.FinMeasAdditive μ (T + T')
theorem
MeasureTheory.FinMeasAdditive.smul
{α : Type u_1}
{𝕜 : Type u_6}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[AddCommMonoid β]
{T : Set α → β}
[Monoid 𝕜]
[DistribMulAction 𝕜 β]
(hT : MeasureTheory.FinMeasAdditive μ T)
(c : 𝕜)
:
MeasureTheory.FinMeasAdditive μ fun (s : Set α) => c • T s
theorem
MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[AddCommMonoid β]
{T : Set α → β}
{μ' : MeasureTheory.Measure α}
(h : ∀ (s : Set α), MeasurableSet s → μ s = ⊤ → μ' s = ⊤)
(hT : MeasureTheory.FinMeasAdditive μ T)
:
theorem
MeasureTheory.FinMeasAdditive.of_smul_measure
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[AddCommMonoid β]
{T : Set α → β}
(c : ENNReal)
(hc_ne_top : c ≠ ⊤)
(hT : MeasureTheory.FinMeasAdditive (c • μ) T)
:
theorem
MeasureTheory.FinMeasAdditive.smul_measure
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[AddCommMonoid β]
{T : Set α → β}
(c : ENNReal)
(hc_ne_zero : c ≠ 0)
(hT : MeasureTheory.FinMeasAdditive μ T)
:
MeasureTheory.FinMeasAdditive (c • μ) T
theorem
MeasureTheory.FinMeasAdditive.smul_measure_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[AddCommMonoid β]
{T : Set α → β}
(c : ENNReal)
(hc_ne_zero : c ≠ 0)
(hc_ne_top : c ≠ ⊤)
:
MeasureTheory.FinMeasAdditive (c • μ) T ↔ MeasureTheory.FinMeasAdditive μ T
theorem
MeasureTheory.FinMeasAdditive.map_empty_eq_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
[AddCancelMonoid β]
{T : Set α → β}
(hT : MeasureTheory.FinMeasAdditive μ T)
:
theorem
MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[AddCommMonoid β]
(T : Set α → β)
(T_empty : T ∅ = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
{ι : Type u_8}
(S : ι → Set α)
(sι : Finset ι)
(hS_meas : ∀ (i : ι), MeasurableSet (S i))
(hSp : ∀ i ∈ sι, μ (S i) ≠ ⊤)
(h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j))
:
T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
def
MeasureTheory.DominatedFinMeasAdditive
{α : Type u_1}
{β : Type u_7}
[SeminormedAddCommGroup β]
:
{x : MeasurableSpace α} → MeasureTheory.Measure α → (Set α → β) → ℝ → Prop
A FinMeasAdditive set function whose norm on every set is less than the measure of the
set (up to a multiplicative constant).
Equations
- MeasureTheory.DominatedFinMeasAdditive μ T C = (MeasureTheory.FinMeasAdditive μ T ∧ ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal)
Instances For
theorem
MeasureTheory.DominatedFinMeasAdditive.zero
{α : Type u_1}
{β : Type u_7}
[SeminormedAddCommGroup β]
{C : ℝ}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(hC : 0 ≤ C)
:
theorem
MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
[NormedAddCommGroup β]
{T : Set α → β}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{s : Set α}
(hs : MeasurableSet s)
(hs_zero : μ s = 0)
:
T s = 0
theorem
MeasureTheory.DominatedFinMeasAdditive.eq_zero
{α : Type u_1}
{β : Type u_8}
[NormedAddCommGroup β]
{T : Set α → β}
{C : ℝ}
{m : MeasurableSpace α}
(hT : MeasureTheory.DominatedFinMeasAdditive 0 T C)
{s : Set α}
(hs : MeasurableSet s)
:
T s = 0
theorem
MeasureTheory.DominatedFinMeasAdditive.add
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[SeminormedAddCommGroup β]
{T : Set α → β}
{T' : Set α → β}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
:
MeasureTheory.DominatedFinMeasAdditive μ (T + T') (C + C')
theorem
MeasureTheory.DominatedFinMeasAdditive.smul
{α : Type u_1}
{𝕜 : Type u_6}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[SeminormedAddCommGroup β]
{T : Set α → β}
{C : ℝ}
[NormedField 𝕜]
[NormedSpace 𝕜 β]
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(c : 𝕜)
:
theorem
MeasureTheory.DominatedFinMeasAdditive.of_measure_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[SeminormedAddCommGroup β]
{T : Set α → β}
{C : ℝ}
{μ' : MeasureTheory.Measure α}
(h : μ ≤ μ')
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hC : 0 ≤ C)
:
theorem
MeasureTheory.DominatedFinMeasAdditive.add_measure_right
{α : Type u_1}
{β : Type u_7}
[SeminormedAddCommGroup β]
{T : Set α → β}
{C : ℝ}
:
∀ {x : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
MeasureTheory.DominatedFinMeasAdditive μ T C → 0 ≤ C → MeasureTheory.DominatedFinMeasAdditive (μ + ν) T C
theorem
MeasureTheory.DominatedFinMeasAdditive.add_measure_left
{α : Type u_1}
{β : Type u_7}
[SeminormedAddCommGroup β]
{T : Set α → β}
{C : ℝ}
:
∀ {x : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
MeasureTheory.DominatedFinMeasAdditive ν T C → 0 ≤ C → MeasureTheory.DominatedFinMeasAdditive (μ + ν) T C
theorem
MeasureTheory.DominatedFinMeasAdditive.of_smul_measure
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[SeminormedAddCommGroup β]
{T : Set α → β}
{C : ℝ}
(c : ENNReal)
(hc_ne_top : c ≠ ⊤)
(hT : MeasureTheory.DominatedFinMeasAdditive (c • μ) T C)
:
MeasureTheory.DominatedFinMeasAdditive μ T (c.toReal * C)
theorem
MeasureTheory.DominatedFinMeasAdditive.of_measure_le_smul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[SeminormedAddCommGroup β]
{T : Set α → β}
{C : ℝ}
{μ' : MeasureTheory.Measure α}
(c : ENNReal)
(hc : c ≠ ⊤)
(h : μ ≤ c • μ')
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hC : 0 ≤ C)
:
MeasureTheory.DominatedFinMeasAdditive μ' T (c.toReal * C)
def
MeasureTheory.SimpleFunc.setToSimpleFunc
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
:
{x : MeasurableSpace α} → (Set α → F →L[ℝ] F') → MeasureTheory.SimpleFunc α F → F'
Extend Set α → (F →L[ℝ] F') to (α →ₛ F) → F'.
Equations
- MeasureTheory.SimpleFunc.setToSimpleFunc T f = ∑ x_1 ∈ f.range, (T (↑f ⁻¹' {x_1})) x_1
Instances For
@[simp]
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_zero
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m : MeasurableSpace α}
(f : MeasureTheory.SimpleFunc α F)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_zero'
{α : Type u_1}
{E : Type u_2}
{F' : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F'}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0)
(f : MeasureTheory.SimpleFunc α E)
(hf : MeasureTheory.Integrable (↑f) μ)
:
@[simp]
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_zero_apply
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m : MeasurableSpace α}
(T : Set α → F →L[ℝ] F')
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m : MeasurableSpace α}
(T : Set α → F →L[ℝ] F')
(f : MeasureTheory.SimpleFunc α F)
:
MeasureTheory.SimpleFunc.setToSimpleFunc T f = ∑ x ∈ Finset.filter (fun (x : F) => x ≠ 0) f.range, (T (↑f ⁻¹' {x})) x
theorem
MeasureTheory.SimpleFunc.map_setToSimpleFunc
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
{G : Type u_5}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[NormedAddCommGroup G]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → F →L[ℝ] F')
(h_add : MeasureTheory.FinMeasAdditive μ T)
{f : MeasureTheory.SimpleFunc α G}
(hf : MeasureTheory.Integrable (↑f) μ)
{g : G → F}
(hg : g 0 = 0)
:
MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.map g f) = ∑ x ∈ f.range, (T (↑f ⁻¹' {x})) (g x)
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_congr'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(h_add : MeasureTheory.FinMeasAdditive μ T)
{f : MeasureTheory.SimpleFunc α E}
{g : MeasureTheory.SimpleFunc α E}
(hf : MeasureTheory.Integrable (↑f) μ)
(hg : MeasureTheory.Integrable (↑g) μ)
(h : Pairwise fun (x y : E) => T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_congr
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
{f : MeasureTheory.SimpleFunc α E}
{g : MeasureTheory.SimpleFunc α E}
(hf : MeasureTheory.Integrable (↑f) μ)
(h : ↑f =ᵐ[μ] ↑g)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_congr_left
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(T' : Set α → E →L[ℝ] F)
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s)
(f : MeasureTheory.SimpleFunc α E)
(hf : MeasureTheory.Integrable (↑f) μ)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_add_left
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m : MeasurableSpace α}
(T : Set α → F →L[ℝ] F')
(T' : Set α → F →L[ℝ] F')
{f : MeasureTheory.SimpleFunc α F}
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_add_left'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(T' : Set α → E →L[ℝ] F)
(T'' : Set α → E →L[ℝ] F)
(h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s)
{f : MeasureTheory.SimpleFunc α E}
(hf : MeasureTheory.Integrable (↑f) μ)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m : MeasurableSpace α}
(T : Set α → F →L[ℝ] F')
(c : ℝ)
(f : MeasureTheory.SimpleFunc α F)
:
MeasureTheory.SimpleFunc.setToSimpleFunc (fun (s : Set α) => c • T s) f = c • MeasureTheory.SimpleFunc.setToSimpleFunc T f
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left'
{α : Type u_1}
{E : Type u_2}
{F' : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F')
(T' : Set α → E →L[ℝ] F')
(c : ℝ)
(h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s)
{f : MeasureTheory.SimpleFunc α E}
(hf : MeasureTheory.Integrable (↑f) μ)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_add
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(h_add : MeasureTheory.FinMeasAdditive μ T)
{f : MeasureTheory.SimpleFunc α E}
{g : MeasureTheory.SimpleFunc α E}
(hf : MeasureTheory.Integrable (↑f) μ)
(hg : MeasureTheory.Integrable (↑g) μ)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_neg
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(h_add : MeasureTheory.FinMeasAdditive μ T)
{f : MeasureTheory.SimpleFunc α E}
(hf : MeasureTheory.Integrable (↑f) μ)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_sub
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(h_add : MeasureTheory.FinMeasAdditive μ T)
{f : MeasureTheory.SimpleFunc α E}
{g : MeasureTheory.SimpleFunc α E}
(hf : MeasureTheory.Integrable (↑f) μ)
(hg : MeasureTheory.Integrable (↑g) μ)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_smul_real
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(c : ℝ)
{f : MeasureTheory.SimpleFunc α E}
(hf : MeasureTheory.Integrable (↑f) μ)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_smul
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_6}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_7}
[NormedAddCommGroup E]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace ℝ E]
[NormedSpace 𝕜 F]
(T : Set α → E →L[ℝ] F)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
(c : 𝕜)
{f : MeasureTheory.SimpleFunc α E}
(hf : MeasureTheory.Integrable (↑f) μ)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left
{α : Type u_1}
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
{m : MeasurableSpace α}
(T : Set α → F →L[ℝ] G'')
(T' : Set α → F →L[ℝ] G'')
(hTT' : ∀ (s : Set α) (x : F), (T s) x ≤ (T' s) x)
(f : MeasureTheory.SimpleFunc α F)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left'
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
(T : Set α → E →L[ℝ] G'')
(T' : Set α → E →L[ℝ] G'')
(hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x)
(f : MeasureTheory.SimpleFunc α E)
(hf : MeasureTheory.Integrable (↑f) μ)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg
{α : Type u_1}
{G' : Type u_7}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[NormedLatticeAddCommGroup G']
[NormedSpace ℝ G']
{m : MeasurableSpace α}
(T : Set α → G' →L[ℝ] G'')
(hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x)
(f : MeasureTheory.SimpleFunc α G')
(hf : 0 ≤ f)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[NormedLatticeAddCommGroup G']
[NormedSpace ℝ G']
(T : Set α → G' →L[ℝ] G'')
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
(f : MeasureTheory.SimpleFunc α G')
(hf : 0 ≤ f)
(hfi : MeasureTheory.Integrable (↑f) μ)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_mono
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[NormedLatticeAddCommGroup G']
[NormedSpace ℝ G']
{T : Set α → G' →L[ℝ] G''}
(h_add : MeasureTheory.FinMeasAdditive μ T)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f : MeasureTheory.SimpleFunc α G'}
{g : MeasureTheory.SimpleFunc α G'}
(hfi : MeasureTheory.Integrable (↑f) μ)
(hgi : MeasureTheory.Integrable (↑g) μ)
(hfg : f ≤ g)
:
theorem
MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m : MeasurableSpace α}
(T : Set α → F' →L[ℝ] F)
(f : MeasureTheory.SimpleFunc α F')
:
@[deprecated MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm]
theorem
MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_op_norm
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m : MeasurableSpace α}
(T : Set α → F' →L[ℝ] F)
(f : MeasureTheory.SimpleFunc α F')
:
Alias of MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm.
theorem
MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → F →L[ℝ] F')
{C : ℝ}
(hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal)
(f : MeasureTheory.SimpleFunc α F)
:
theorem
MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable
{α : Type u_1}
{E : Type u_2}
{F' : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F')
{C : ℝ}
(hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal)
(f : MeasureTheory.SimpleFunc α E)
(hf : MeasureTheory.Integrable (↑f) μ)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_indicator
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
(T : Set α → F →L[ℝ] F')
(hT_empty : T ∅ = 0)
{m : MeasurableSpace α}
{s : Set α}
(hs : MeasurableSet s)
(x : F)
:
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_const'
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[Nonempty α]
(T : Set α → F →L[ℝ] F')
(x : F)
{m : MeasurableSpace α}
:
MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.const α x) = (T Set.univ) x
theorem
MeasureTheory.SimpleFunc.setToSimpleFunc_const
{α : Type u_1}
{F : Type u_3}
{F' : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup F']
[NormedSpace ℝ F']
(T : Set α → F →L[ℝ] F')
(hT_empty : T ∅ = 0)
(x : F)
{m : MeasurableSpace α}
:
MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.const α x) = (T Set.univ) x
theorem
MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul
{α : Type u_1}
{G : Type u_5}
[NormedAddCommGroup G]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(f : ↥(MeasureTheory.Lp.simpleFunc G 1 μ))
:
‖f‖ = ∑ x ∈ (MeasureTheory.Lp.simpleFunc.toSimpleFunc f).range,
(μ (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖
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 α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
F
Extend Set α → (E →L[ℝ] F') to (α →₁ₛ[μ] E) → F'.
Equations
Instances For
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 α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
{f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)}
{g : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)}
(h : ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) =ᵐ[μ] ↑(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(T' : Set α → E →L[ℝ] F)
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{μ' : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(hμ : μ.AbsolutelyContinuous μ')
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
(f' : ↥(MeasureTheory.Lp.simpleFunc E 1 μ'))
(h : ↑↑↑f =ᵐ[μ] ↑↑↑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 α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(T' : Set α → E →L[ℝ] F)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(T' : Set α → E →L[ℝ] F)
(T'' : Set α → E →L[ℝ] F)
(h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(c : ℝ)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
MeasureTheory.L1.SimpleFunc.setToL1S (fun (s : Set α) => c • T s) f = c • MeasureTheory.L1.SimpleFunc.setToL1S T f
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 α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(T' : Set α → E →L[ℝ] F)
(c : ℝ)
(h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
(g : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
(g : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(c : ℝ)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[NormedField 𝕜]
{E : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
(T : Set α → E →L[ℝ] F)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
(c : 𝕜)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F)
{C : ℝ}
(hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
{s : Set α}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(hs : MeasurableSet s)
(hμs : μ s < ⊤)
(x : E)
:
MeasureTheory.L1.SimpleFunc.setToL1S T (MeasureTheory.Lp.simpleFunc.indicatorConst 1 hs ⋯ x) = (T s) x
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 α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{T : Set α → E →L[ℝ] F}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(x : E)
:
MeasureTheory.L1.SimpleFunc.setToL1S T (MeasureTheory.Lp.simpleFunc.indicatorConst 1 ⋯ ⋯ x) = (T Set.univ) x
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_mono_left
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G'' : Type u_7}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
{T : Set α → E →L[ℝ] G''}
{T' : Set α → E →L[ℝ] G''}
(hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_mono_left'
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G'' : Type u_7}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
{T : Set α → E →L[ℝ] G''}
{T' : Set α → E →L[ℝ] G''}
(hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G'' : Type u_7}
{G' : Type u_8}
[NormedLatticeAddCommGroup G']
[NormedSpace ℝ G']
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
{T : Set α → G'' →L[ℝ] G'}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x)
{f : ↥(MeasureTheory.Lp.simpleFunc G'' 1 μ)}
(hf : 0 ≤ f)
:
theorem
MeasureTheory.L1.SimpleFunc.setToL1S_mono
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G'' : Type u_7}
{G' : Type u_8}
[NormedLatticeAddCommGroup G']
[NormedSpace ℝ G']
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
{T : Set α → G'' →L[ℝ] G'}
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0)
(h_add : MeasureTheory.FinMeasAdditive μ T)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x)
{f : ↥(MeasureTheory.Lp.simpleFunc G'' 1 μ)}
{g : ↥(MeasureTheory.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 α}
(μ : MeasureTheory.Measure α)
[NormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
:
↥(MeasureTheory.Lp.simpleFunc E 1 μ) →L[𝕜] F
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 ⋯
Instances For
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 α}
(μ : MeasureTheory.Measure α)
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
:
↥(MeasureTheory.Lp.simpleFunc E 1 μ) →L[ℝ] F
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 ⋯
Instances For
@[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 α}
{μ : MeasureTheory.Measure α}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ 0 C)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f = 0
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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f = 0
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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(h : T = T')
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
{μ' : MeasureTheory.Measure α}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ' T C')
(hμ : μ.AbsolutelyContinuous μ')
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
(f' : ↥(MeasureTheory.Lp.simpleFunc E 1 μ'))
(h : ↑↑↑f =ᵐ[μ] ↑↑↑f')
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ' hT') 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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ ⋯) f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f + (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') 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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{T'' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
{C'' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(hT'' : MeasureTheory.DominatedFinMeasAdditive μ T'' C'')
(h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT'') f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f + (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(c : ℝ)
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ ⋯) f = c • (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f
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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
(c : ℝ)
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f = c • (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f
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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hC : 0 ≤ C)
:
‖MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT‖ ≤ 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 α}
{μ : MeasureTheory.Measure α}
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
:
‖MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT‖ ≤ max C 0
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 α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(x : E)
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) (MeasureTheory.Lp.simpleFunc.indicatorConst 1 ⋯ ⋯ x) = (T Set.univ) x
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
{T : Set α → E →L[ℝ] G''}
{T' : Set α → E →L[ℝ] G''}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left'
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
{T : Set α → E →L[ℝ] G''}
{T' : Set α → E →L[ℝ] G''}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[NormedLatticeAddCommGroup G']
[NormedSpace ℝ G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f : ↥(MeasureTheory.Lp.simpleFunc G' 1 μ)}
(hf : 0 ≤ f)
:
0 ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α G' μ hT) f
theorem
MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[NormedLatticeAddCommGroup G']
[NormedSpace ℝ G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f : ↥(MeasureTheory.Lp.simpleFunc G' 1 μ)}
{g : ↥(MeasureTheory.Lp.simpleFunc G' 1 μ)}
(hfg : f ≤ g)
:
(MeasureTheory.L1.SimpleFunc.setToL1SCLM α G' μ hT) f ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α G' μ hT) 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 α}
{μ : MeasureTheory.Measure α}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
:
↥(MeasureTheory.Lp E 1 μ) →L[𝕜] F
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 𝕜) ⋯ ⋯
Instances For
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
:
↥(MeasureTheory.Lp E 1 μ) →L[ℝ] F
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 ℝ) ⋯ ⋯
Instances For
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ))
:
(MeasureTheory.L1.setToL1 hT) ↑f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f
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 α}
{μ : MeasureTheory.Measure α}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 hT) f = (MeasureTheory.L1.setToL1' 𝕜 hT h_smul) f
@[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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ 0 C)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 hT) f = 0
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 hT) f = 0
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
(T : Set α → E →L[ℝ] F)
(T' : Set α → E →L[ℝ] F)
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(h : T = T')
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 hT) f = (MeasureTheory.L1.setToL1 hT') f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
(T : Set α → E →L[ℝ] F)
(T' : Set α → E →L[ℝ] F)
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 hT) f = (MeasureTheory.L1.setToL1 hT') f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 ⋯) f = (MeasureTheory.L1.setToL1 hT) f + (MeasureTheory.L1.setToL1 hT') f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{T'' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
{C'' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(hT'' : MeasureTheory.DominatedFinMeasAdditive μ T'' C'')
(h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 hT'') f = (MeasureTheory.L1.setToL1 hT) f + (MeasureTheory.L1.setToL1 hT') f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(c : ℝ)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 ⋯) f = c • (MeasureTheory.L1.setToL1 hT) f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(c : ℝ)
(h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 hT') f = c • (MeasureTheory.L1.setToL1 hT) f
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 α}
{μ : MeasureTheory.Measure α}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
(c : 𝕜)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 hT) (c • f) = c • (MeasureTheory.L1.setToL1 hT) f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s < ⊤)
(x : E)
:
(MeasureTheory.L1.setToL1 hT) ↑(MeasureTheory.Lp.simpleFunc.indicatorConst 1 hs ⋯ x) = (T s) x
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : E)
:
(MeasureTheory.L1.setToL1 hT) (MeasureTheory.indicatorConstLp 1 hs hμs x) = (T s) x
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(x : E)
:
(MeasureTheory.L1.setToL1 hT) (MeasureTheory.indicatorConstLp 1 ⋯ ⋯ x) = (T Set.univ) x
theorem
MeasureTheory.L1.setToL1_mono_left'
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
{T : Set α → E →L[ℝ] G''}
{T' : Set α → E →L[ℝ] G''}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 hT) f ≤ (MeasureTheory.L1.setToL1 hT') f
theorem
MeasureTheory.L1.setToL1_mono_left
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
{T : Set α → E →L[ℝ] G''}
{T' : Set α → E →L[ℝ] G''}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
(MeasureTheory.L1.setToL1 hT) f ≤ (MeasureTheory.L1.setToL1 hT') f
theorem
MeasureTheory.L1.setToL1_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
[NormedLatticeAddCommGroup G']
[NormedSpace ℝ G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f : ↥(MeasureTheory.Lp G' 1 μ)}
(hf : 0 ≤ f)
:
0 ≤ (MeasureTheory.L1.setToL1 hT) f
theorem
MeasureTheory.L1.setToL1_mono
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
[NormedLatticeAddCommGroup G']
[NormedSpace ℝ G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f : ↥(MeasureTheory.Lp G' 1 μ)}
{g : ↥(MeasureTheory.Lp G' 1 μ)}
(hfg : f ≤ g)
:
(MeasureTheory.L1.setToL1 hT) f ≤ (MeasureTheory.L1.setToL1 hT) 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hC : 0 ≤ C)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
:
‖MeasureTheory.L1.setToL1 hT‖ ≤ max C 0
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
:
LipschitzWith C.toNNReal ⇑(MeasureTheory.L1.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(f : ↥(MeasureTheory.Lp E 1 μ))
{ι : Type u_7}
(fs : ι → ↥(MeasureTheory.Lp E 1 μ))
{l : Filter ι}
(hfs : Filter.Tendsto fs l (nhds f))
:
Filter.Tendsto (fun (i : ι) => (MeasureTheory.L1.setToL1 hT) (fs i)) l (nhds ((MeasureTheory.L1.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 α}
(μ : MeasureTheory.Measure α)
[CompleteSpace F]
(T : Set α → E →L[ℝ] F)
{C : ℝ}
(hT : MeasureTheory.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
Instances For
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.setToFun μ T hT f = (MeasureTheory.L1.setToL1 hT) (MeasureTheory.Integrable.toL1 f hf)
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
MeasureTheory.setToFun μ T hT ↑↑f = (MeasureTheory.L1.setToL1 hT) f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hf : ¬MeasureTheory.Integrable f μ)
:
MeasureTheory.setToFun μ T hT f = 0
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hf : ¬MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.setToFun μ T hT f = 0
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(h : T = T')
(f : α → E)
:
MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ T' hT' 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s)
(f : α → E)
:
MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ T' hT' f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(f : α → E)
:
MeasureTheory.setToFun μ (T + T') ⋯ f = MeasureTheory.setToFun μ T hT f + MeasureTheory.setToFun μ T' hT' f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{T'' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
{C'' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(hT'' : MeasureTheory.DominatedFinMeasAdditive μ T'' C'')
(h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s)
(f : α → E)
:
MeasureTheory.setToFun μ T'' hT'' f = MeasureTheory.setToFun μ T hT f + MeasureTheory.setToFun μ T' hT' f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(c : ℝ)
(f : α → E)
:
MeasureTheory.setToFun μ (fun (s : Set α) => c • T s) ⋯ f = c • MeasureTheory.setToFun μ T hT f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{T' : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(c : ℝ)
(h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s)
(f : α → E)
:
MeasureTheory.setToFun μ T' hT' f = c • MeasureTheory.setToFun μ T hT f
@[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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
:
MeasureTheory.setToFun μ T hT 0 = 0
@[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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{C : ℝ}
{f : α → E}
{hT : MeasureTheory.DominatedFinMeasAdditive μ 0 C}
:
MeasureTheory.setToFun μ 0 hT f = 0
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0)
:
MeasureTheory.setToFun μ T hT f = 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
{g : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.setToFun μ T hT (f + g) = MeasureTheory.setToFun μ T hT f + MeasureTheory.setToFun μ T hT 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{ι : Type u_7}
(s : Finset ι)
{f : ι → α → E}
(hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ)
:
MeasureTheory.setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, MeasureTheory.setToFun μ T hT (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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{ι : Type u_7}
(s : Finset ι)
{f : ι → α → E}
(hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ)
:
(MeasureTheory.setToFun μ T hT fun (a : α) => ∑ i ∈ s, f i a) = ∑ i ∈ s, MeasureTheory.setToFun μ T hT (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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(f : α → E)
:
MeasureTheory.setToFun μ T hT (-f) = -MeasureTheory.setToFun μ T hT f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
{g : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.setToFun μ T hT (f - g) = MeasureTheory.setToFun μ T hT f - MeasureTheory.setToFun μ T hT 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x)
(c : 𝕜)
(f : α → E)
:
MeasureTheory.setToFun μ T hT (c • f) = c • MeasureTheory.setToFun μ T hT f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
{g : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(h : f =ᵐ[μ] g)
:
MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ T hT 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(h : μ = 0)
:
MeasureTheory.setToFun μ T hT f = 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → μ s = 0)
:
MeasureTheory.setToFun μ T hT f = 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.setToFun μ T hT ↑↑(MeasureTheory.Integrable.toL1 f hf) = MeasureTheory.setToFun μ T hT 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : E)
:
MeasureTheory.setToFun μ T hT (s.indicator fun (x_1 : α) => x) = (T s) x
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(x : E)
:
(MeasureTheory.setToFun μ T hT fun (x_1 : α) => x) = (T Set.univ) x
theorem
MeasureTheory.setToFun_mono_left'
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
{T : Set α → E →L[ℝ] G''}
{T' : Set α → E →L[ℝ] G''}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x)
(f : α → E)
:
MeasureTheory.setToFun μ T hT f ≤ MeasureTheory.setToFun μ T' hT' f
theorem
MeasureTheory.setToFun_mono_left
{α : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
{T : Set α → E →L[ℝ] G''}
{T' : Set α → E →L[ℝ] G''}
{C : ℝ}
{C' : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
(hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x)
(f : ↥(MeasureTheory.Lp E 1 μ))
:
MeasureTheory.setToFun μ T hT ↑↑f ≤ MeasureTheory.setToFun μ T' hT' ↑↑f
theorem
MeasureTheory.setToFun_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
[NormedLatticeAddCommGroup G']
[NormedSpace ℝ G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f : α → G'}
(hf : 0 ≤ᵐ[μ] f)
:
0 ≤ MeasureTheory.setToFun μ T hT f
theorem
MeasureTheory.setToFun_mono
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{G' : Type u_7}
{G'' : Type u_8}
[NormedLatticeAddCommGroup G'']
[NormedSpace ℝ G'']
[CompleteSpace G'']
[NormedLatticeAddCommGroup G']
[NormedSpace ℝ G']
{T : Set α → G' →L[ℝ] G''}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x)
{f : α → G'}
{g : α → G'}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
(hfg : f ≤ᵐ[μ] g)
:
MeasureTheory.setToFun μ T hT f ≤ MeasureTheory.setToFun μ T hT 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
:
Continuous fun (f : ↥(MeasureTheory.Lp E 1 μ)) => MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{ι : Type u_7}
(f : α → E)
(hfi : MeasureTheory.Integrable f μ)
{fs : ι → α → E}
{l : Filter ι}
(hfsi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (fs i) μ)
(hfs : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), ↑‖fs i x - f x‖₊ ∂μ) l (nhds 0))
:
Filter.Tendsto (fun (i : ι) => MeasureTheory.setToFun μ T hT (fs i)) l (nhds (MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
[MeasurableSpace E]
[BorelSpace E]
{f : α → E}
{s : Set E}
[TopologicalSpace.SeparableSpace ↑s]
(hfi : MeasureTheory.Integrable f μ)
(hfm : Measurable f)
(hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s)
{y₀ : E}
(h₀ : y₀ ∈ s)
(h₀i : MeasureTheory.Integrable (fun (x : α) => y₀) μ)
:
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.setToFun μ T hT ↑(MeasureTheory.SimpleFunc.approxOn f hfm s y₀ h₀ n))
Filter.atTop (nhds (MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
[MeasurableSpace E]
[BorelSpace E]
{f : α → E}
(fmeas : Measurable f)
(hf : MeasureTheory.Integrable f μ)
(s : Set E)
[TopologicalSpace.SeparableSpace ↑s]
(hs : Set.range f ∪ {0} ⊆ s)
:
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.setToFun μ T hT ↑(MeasureTheory.SimpleFunc.approxOn f fmeas s 0 ⋯ n))
Filter.atTop (nhds (MeasureTheory.setToFun μ T hT f))
theorem
MeasureTheory.continuous_L1_toL1
{α : Type u_1}
{G : Type u_5}
[NormedAddCommGroup G]
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{μ' : MeasureTheory.Measure α}
(c' : ENNReal)
(hc' : c' ≠ ⊤)
(hμ'_le : μ' ≤ c' • μ)
:
Continuous fun (f : ↥(MeasureTheory.Lp G 1 μ)) => MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
{μ' : MeasureTheory.Measure α}
(c' : ENNReal)
(hc' : c' ≠ ⊤)
(hμ'_le : μ' ≤ c' • μ)
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ' T C')
(f : α → E)
(hfμ : MeasureTheory.Integrable f μ)
:
MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ' T hT' 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
{μ' : MeasureTheory.Measure α}
(c : ENNReal)
(c' : ENNReal)
(hc : c ≠ ⊤)
(hc' : c' ≠ ⊤)
(hμ_le : μ ≤ c • μ')
(hμ'_le : μ' ≤ c' • μ)
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT' : MeasureTheory.DominatedFinMeasAdditive μ' T C')
(f : α → E)
:
MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ' T hT' f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
{μ' : MeasureTheory.Measure α}
(hT_add : MeasureTheory.DominatedFinMeasAdditive (μ + μ') T C')
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(f : α → E)
(hf : MeasureTheory.Integrable f (μ + μ'))
:
MeasureTheory.setToFun (μ + μ') T hT_add f = MeasureTheory.setToFun μ T hT 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
{μ' : MeasureTheory.Measure α}
(hT_add : MeasureTheory.DominatedFinMeasAdditive (μ + μ') T C')
(hT : MeasureTheory.DominatedFinMeasAdditive μ' T C)
(f : α → E)
(hf : MeasureTheory.Integrable f (μ + μ'))
:
MeasureTheory.setToFun (μ + μ') T hT_add f = MeasureTheory.setToFun μ' T hT 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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive (⊤ • μ) T C)
(f : α → E)
:
MeasureTheory.setToFun (⊤ • μ) T hT f = 0
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{C' : ℝ}
(c : ENNReal)
(hc_ne_top : c ≠ ⊤)
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hT_smul : MeasureTheory.DominatedFinMeasAdditive (c • μ) T C')
(f : α → E)
:
MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun (c • μ) T hT_smul f
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(f : ↥(MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hf : MeasureTheory.Integrable f μ)
(hC : 0 ≤ C)
:
‖MeasureTheory.setToFun μ T hT f‖ ≤ C * ‖MeasureTheory.Integrable.toL1 f hf‖
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{f : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
(hf : MeasureTheory.Integrable f μ)
:
‖MeasureTheory.setToFun μ T hT f‖ ≤ max C 0 * ‖MeasureTheory.Integrable.toL1 f hf‖
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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{fs : ℕ → α → E}
{f : α → E}
(bound : α → ℝ)
(fs_measurable : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fs n) μ)
(bound_integrable : MeasureTheory.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 : ℕ) => MeasureTheory.setToFun μ T hT (fs n)) Filter.atTop
(nhds (MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{ι : Type u_7}
{l : Filter ι}
[l.IsCountablyGenerated]
{fs : ι → α → E}
{f : α → E}
(bound : α → ℝ)
(hfs_meas : ∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (fs n) μ)
(h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a)
(bound_integrable : MeasureTheory.Integrable bound μ)
(h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ι) => fs n a) l (nhds (f a)))
:
Filter.Tendsto (fun (n : ι) => MeasureTheory.setToFun μ T hT (fs n)) l (nhds (MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_7}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{x₀ : X}
{bound : α → ℝ}
{s : Set X}
(hfs_meas : ∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : MeasureTheory.Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun (x : X) => fs x a) s x₀)
:
ContinuousWithinAt (fun (x : X) => MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_7}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{x₀ : X}
{bound : α → ℝ}
(hfs_meas : ∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : MeasureTheory.Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun (x : X) => fs x a) x₀)
:
ContinuousAt (fun (x : X) => MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_7}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{bound : α → ℝ}
{s : Set X}
(hfs_meas : ∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : MeasureTheory.Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun (x : X) => fs x a) s)
:
ContinuousOn (fun (x : X) => MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[CompleteSpace F]
{T : Set α → E →L[ℝ] F}
{C : ℝ}
{X : Type u_7}
[TopologicalSpace X]
[FirstCountableTopology X]
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{fs : X → α → E}
{bound : α → ℝ}
(hfs_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : MeasureTheory.Integrable bound μ)
(h_cont : ∀ᵐ (a : α) ∂μ, Continuous fun (x : X) => fs x a)
:
Continuous fun (x : X) => MeasureTheory.setToFun μ T hT (fs x)