Indicator of a set as an element of Lp

For a set s with (hs : MeasurableSet s) and (hμs : μ s < ∞), we build indicatorConstLp p hs hμs c, the element of Lp corresponding to s.indicator (fun _ => c).

Main definitions

• MeasureTheory.indicatorConstLp: Indicator of a set as an element of Lp.
• MeasureTheory.Lp.const: Constant function as an element of Lp for a finite measure.

theorem MeasureTheory.exists_eLpNorm_indicator_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (hp : p ≠ ⊤) (c : E) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (η : NNReal), 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun (x : α) => c) p μ ≤ ε

The eLpNorm of the indicator of a set is uniformly small if the set itself has small measure, for any p < ∞. Given here as an existential ∀ ε > 0, ∃ η > 0, ... to avoid later management of ℝ≥0∞-arithmetic.

theorem HasCompactSupport.memLp_of_bound {E : Type u_2} {p : ENNReal} [NormedAddCommGroup E] {X : Type u_3} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → E} (hf : HasCompactSupport f) (h2f : MeasureTheory.AEStronglyMeasurable f μ) (C : ℝ) (hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C) : MeasureTheory.MemLp f p μ

A bounded measurable function with compact support is in L^p.

theorem Continuous.memLp_of_hasCompactSupport {E : Type u_2} {p : ENNReal} [NormedAddCommGroup E] {X : Type u_3} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [OpensMeasurableSpace X] {f : X → E} (hf : Continuous f) (h'f : HasCompactSupport f) : MeasureTheory.MemLp f p μ

A continuous function with compact support is in L^p.

def MeasureTheory.indicatorConstLp {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} (p : ENNReal) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : E) : ↥(Lp E p μ)

Indicator of a set as an element of Lp.

Equations

• MeasureTheory.indicatorConstLp p hs hμs c = MeasureTheory.MemLp.toLp (s.indicator fun (x : α) => c) ⋯

theorem MeasureTheory.indicatorConstLp_add {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c c' : E} : indicatorConstLp p hs hμs c + indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c + c')

A version of Set.indicator_add for MeasureTheory.indicatorConstLp

theorem MeasureTheory.indicatorConstLp_sub {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c c' : E} : indicatorConstLp p hs hμs c - indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c - c')

A version of Set.indicator_sub for MeasureTheory.indicatorConstLp

theorem MeasureTheory.indicatorConstLp_coeFn {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ↑↑(indicatorConstLp p hs hμs c) =ᶠ[ae μ] s.indicator fun (x : α) => c

theorem MeasureTheory.indicatorConstLp_coeFn_mem {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp p hs hμs c) x = c

theorem MeasureTheory.indicatorConstLp_coeFn_notMem {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ∀ᵐ (x : α) ∂μ, x ∉ s → ↑↑(indicatorConstLp p hs hμs c) x = 0

theorem MeasureTheory.norm_indicatorConstLp {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) : ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)

theorem MeasureTheory.norm_indicatorConstLp_top {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} (hμs_ne_zero : μ s ≠ 0) : ‖indicatorConstLp ⊤ hs hμs c‖ = ‖c‖

theorem MeasureTheory.norm_indicatorConstLp' {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} (hp_pos : p ≠ 0) (hμs_pos : μ s ≠ 0) : ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)

theorem MeasureTheory.norm_indicatorConstLp_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ‖indicatorConstLp p hs hμs c‖ ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)

theorem MeasureTheory.nnnorm_indicatorConstLp_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ‖indicatorConstLp p hs hμs c‖₊ ≤ ‖c‖₊ * (μ s).toNNReal ^ (1 / p.toReal)

theorem MeasureTheory.enorm_indicatorConstLp_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ‖indicatorConstLp p hs hμs c‖ₑ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

theorem MeasureTheory.edist_indicatorConstLp_eq_enorm {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} {t : Set α} {ht : MeasurableSet t} {hμt : μ t ≠ ⊤} : edist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) = ‖indicatorConstLp p ⋯ ⋯ c‖ₑ

theorem MeasureTheory.dist_indicatorConstLp_eq_norm {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} {t : Set α} {ht : MeasurableSet t} {hμt : μ t ≠ ⊤} : dist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) = ‖indicatorConstLp p ⋯ ⋯ c‖

theorem MeasureTheory.tendsto_indicatorConstLp_set {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} [hp₁ : Fact (1 ≤ p)] {β : Type u_3} {l : Filter β} {t : β → Set α} {ht : ∀ (b : β), MeasurableSet (t b)} {hμt : ∀ (b : β), μ (t b) ≠ ⊤} (hp : p ≠ ⊤) (h : Filter.Tendsto (fun (b : β) => μ (symmDiff (t b) s)) l (nhds 0)) : Filter.Tendsto (fun (b : β) => indicatorConstLp p ⋯ ⋯ c) l (nhds (indicatorConstLp p hs hμs c))

A family of indicatorConstLp functions tends to an indicatorConstLp, if the underlying sets tend to the set in the sense of the measure of the symmetric difference.

theorem MeasureTheory.continuous_indicatorConstLp_set {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {c : E} [Fact (1 ≤ p)] {X : Type u_3} [TopologicalSpace X] {s : X → Set α} {hs : ∀ (x : X), MeasurableSet (s x)} {hμs : ∀ (x : X), μ (s x) ≠ ⊤} (hp : p ≠ ⊤) (h : ∀ (x : X), Filter.Tendsto (fun (y : X) => μ (symmDiff (s y) (s x))) (nhds x) (nhds 0)) : Continuous fun (x : X) => indicatorConstLp p ⋯ ⋯ c

A family of indicatorConstLp functions is continuous in the parameter, if μ (s y ∆ s x) tends to zero as y tends to x for all x.

@[simp]

theorem MeasureTheory.indicatorConstLp_empty {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {c : E} : indicatorConstLp p ⋯ ⋯ c = 0

theorem MeasureTheory.indicatorConstLp_inj {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s t : Set α} (hs : MeasurableSet s) (hsμ : μ s ≠ ⊤) (ht : MeasurableSet t) (htμ : μ t ≠ ⊤) {c : E} (hc : c ≠ 0) : indicatorConstLp p hs hsμ c = indicatorConstLp p ht htμ c ↔ s =ᶠ[ae μ] t

theorem MeasureTheory.memLp_add_of_disjoint {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f g : α → E} (h : Disjoint (Function.support f) (Function.support g)) (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) : MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ

theorem MeasureTheory.indicatorConstLp_disjoint_union {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤) (hst : Disjoint s t) (c : E) : indicatorConstLp p ⋯ ⋯ c = indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c

The indicator of a disjoint union of two sets is the sum of the indicators of the sets.

def MeasureTheory.Lp.const {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] : E →+ ↥(Lp E p μ)

Constant function as an element of MeasureTheory.Lp for a finite measure.

Equations

• MeasureTheory.Lp.const p μ = { toFun := fun (c : E) => ⟨MeasureTheory.AEEqFun.const α c, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

theorem MeasureTheory.Lp.coeFn_const {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (c : E) : ↑↑((Lp.const p μ) c) =ᶠ[ae μ] Function.const α c

@[simp]

theorem MeasureTheory.Lp.const_val {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (c : E) : ↑((Lp.const p μ) c) = AEEqFun.const α c

@[simp]

theorem MeasureTheory.MemLp.toLp_const {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (c : E) : toLp (fun (x : α) => c) ⋯ = (Lp.const p μ) c

@[simp]

theorem MeasureTheory.indicatorConstLp_univ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (c : E) : indicatorConstLp p ⋯ ⋯ c = (Lp.const p μ) c

theorem MeasureTheory.Lp.norm_const {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (c : E) [NeZero μ] (hp_zero : p ≠ 0) : ‖(Lp.const p μ) c‖ = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

theorem MeasureTheory.Lp.norm_const' {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (c : E) (hp_zero : p ≠ 0) (hp_top : p ≠ ⊤) : ‖(Lp.const p μ) c‖ = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

theorem MeasureTheory.Lp.norm_const_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (c : E) : ‖(Lp.const p μ) c‖ ≤ ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

def MeasureTheory.Lp.constₗ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : E →ₗ[𝕜] ↥(Lp E p μ)

MeasureTheory.Lp.const as a LinearMap.

Equations

• MeasureTheory.Lp.constₗ p μ 𝕜 = { toFun := ⇑(MeasureTheory.Lp.const p μ), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MeasureTheory.Lp.constₗ_apply {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (a : E) : (Lp.constₗ p μ 𝕜) a = (Lp.const p μ) a

def MeasureTheory.Lp.constL {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Fact (1 ≤ p)] : E →L[𝕜] ↥(Lp E p μ)

MeasureTheory.Lp.const as a ContinuousLinearMap.

Equations

• MeasureTheory.Lp.constL p μ 𝕜 = (MeasureTheory.Lp.constₗ p μ 𝕜).mkContinuous (μ.real Set.univ ^ (1 / p.toReal)) ⋯

@[simp]

theorem MeasureTheory.Lp.constL_apply {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Fact (1 ≤ p)] (a : E) : (Lp.constL p μ 𝕜) a = (Lp.const p μ) a

theorem MeasureTheory.Lp.norm_constL_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [IsFiniteMeasure μ] (𝕜 : Type u_3) [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [Fact (1 ≤ p)] : ‖Lp.constL p μ 𝕜‖ ≤ μ.real Set.univ ^ (1 / p.toReal)

theorem MeasureTheory.Lp.indicatorConstLp_compMeasurePreserving {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_3} [MeasurableSpace β] {μb : Measure β} {f : α → β} {s : Set β} (hs : MeasurableSet s) (hμs : μb s ≠ ⊤) (c : E) (hf : MeasurePreserving f μ μb) : (compMeasurePreserving f hf) (indicatorConstLp p hs hμs c) = indicatorConstLp p ⋯ ⋯ c

theorem MeasureTheory.indicatorConstLp_eq_toSpanSingleton_compLp {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} [NormedSpace ℝ E] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E) : indicatorConstLp 2 hs hμs x = (ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)