ℒp seminorms and indicator functions

theorem MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} {s : Set α} (hs : MeasurableSet s) : eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

theorem MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup F] {f : α → F} {s : Set α} (hs : MeasurableSet s) : eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.restrict s)

theorem MeasureTheory.eLpNorm_restrict_le {α : Type u_1} {m0 : MeasurableSpace α} {ε' : Type u_8} [TopologicalSpace ε'] [ContinuousENorm ε'] (f : α → ε') (p : ENNReal) (μ : Measure α) (s : Set α) : eLpNorm f p (μ.restrict s) ≤ eLpNorm f p μ

theorem MeasureTheory.eLpNorm_indicator_le {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} (f : α → ε) : eLpNorm (s.indicator f) p μ ≤ eLpNorm f p μ

theorem MeasureTheory.eLpNormEssSup_indicator_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (s : Set α) (f : α → ε) : eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ

theorem MeasureTheory.eLpNormEssSup_indicator_const_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (s : Set α) (c : ε) : eLpNormEssSup (s.indicator fun (x : α) => c) μ ≤ ‖c‖ₑ

theorem MeasureTheory.eLpNormEssSup_indicator_const_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (s : Set α) (c : ε) (hμs : μ s ≠ 0) : eLpNormEssSup (s.indicator fun (x : α) => c) μ = ‖c‖ₑ

theorem MeasureTheory.eLpNorm_indicator_const₀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {c : ε} {s : Set α} (hs : NullMeasurableSet s μ) (hp : p ≠ 0) (hp_top : p ≠ ⊤) : eLpNorm (s.indicator fun (x : α) => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)

theorem MeasureTheory.eLpNorm_indicator_const {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {c : ε} {s : Set α} (hs : MeasurableSet s) (hp : p ≠ 0) (hp_top : p ≠ ⊤) : eLpNorm (s.indicator fun (x : α) => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)

theorem MeasureTheory.eLpNorm_indicator_const' {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {c : ε} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ 0) (hp : p ≠ 0) : eLpNorm (s.indicator fun (x : α) => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)

theorem MeasureTheory.eLpNorm_indicator_const_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (c : ε) {s : Set α} (p : ENNReal) : eLpNorm (s.indicator fun (x : α) => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

theorem MeasureTheory.MemLp.indicator {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} {f : α → ε} (hs : MeasurableSet s) (hf : MemLp f p μ) : MemLp (s.indicator f) p μ

theorem MeasureTheory.memLp_indicator_iff_restrict {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} {f : α → ε} (hs : MeasurableSet s) : MemLp (s.indicator f) p μ ↔ MemLp f p (μ.restrict s)

theorem MeasureTheory.memLp_indicator_const {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] {s : Set α} (p : ENNReal) (hs : MeasurableSet s) (c : E) (hμsc : c = 0 ∨ μ s ≠ ⊤) : MemLp (s.indicator fun (x : α) => c) p μ

theorem MeasureTheory.eLpNormEssSup_piecewise {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} (f g : α → ε) [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) : eLpNormEssSup (s.piecewise f g) μ = max (eLpNormEssSup f (μ.restrict s)) (eLpNormEssSup g (μ.restrict sᶜ))

theorem MeasureTheory.eLpNorm_top_piecewise {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} (f g : α → ε) [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) : eLpNorm (s.piecewise f g) ⊤ μ = max (eLpNorm f ⊤ (μ.restrict s)) (eLpNorm g ⊤ (μ.restrict sᶜ))

theorem MeasureTheory.MemLp.piecewise {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} {f : α → ε} [DecidablePred fun (x : α) => x ∈ s] {g : α → ε} (hs : MeasurableSet s) (hf : MemLp f p (μ.restrict s)) (hg : MemLp g p (μ.restrict sᶜ)) : MemLp (s.piecewise f g) p μ

theorem MeasureTheory.eLpNorm_indicator_sub_le_of_dist_bdd {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {s : Set α} {β : Type u_9} [NormedAddCommGroup β] (μ : Measure α := by volume_tac) (hp' : p ≠ ⊤) (hs : MeasurableSet s) {f g : α → β} {c : ℝ} (hc : 0 ≤ c) (hf : ∀ x ∈ s, dist (f x) (g x) ≤ c) : eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

theorem MeasureTheory.eLpNorm_sub_le_of_dist_bdd {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {s : Set α} {β : Type u_9} [NormedAddCommGroup β] (μ : Measure α := by volume_tac) (hp : p ≠ ⊤) (hs : MeasurableSet s) {c : ℝ} (hc : 0 ≤ c) {f g : α → β} (h : ∀ (x : α), dist (f x) (g x) ≤ c) (hs₁ : Function.support f ⊆ s) (hs₂ : Function.support g ⊆ s) : eLpNorm (f - g) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

theorem MeasureTheory.MemLp.exists_eLpNorm_indicator_compl_lt {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {β : Type u_7} [NormedAddCommGroup β] (hp_top : p ≠ ⊤) {f : α → β} (hf : MemLp f p μ) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (s : Set α), MeasurableSet s ∧ μ s < ⊤ ∧ eLpNorm (sᶜ.indicator f) p μ < ε

A single function that is MemLp f p μ is tight with respect to μ.