Theorems · Theorem · functional analysis

MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf

∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : SeminormedAddGroup E]
  {ι : Type u_3} [Nonempty ι] [inst_2 : LinearOrder ι] {f : ι → α → E} {f_lim : α → E},
  (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) →
    MeasureTheory.eLpNorm f_lim ⊤ μ = essSup (fun x => Filter.liminf (fun m => ‖f m x‖ₑ) Filter.atTop) μ

Defined in: Mathlib.MeasureTheory.Function.LpSpace.Complete
Cited by: 1 results in Mathlib
Foundations: Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: SeminormedAddGroup Nonempty LinearOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites23

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Top.topstatement · cited by 9,680
LinearOrderstatement and proof · cited by 8,572
nhdsstatement and proof · cited by 5,554
Filter.Tendstostatement and proof · cited by 3,814
Filter.Eventuallystatement and proof · cited by 3,134
Filter.atTopstatement and proof · cited by 2,405
MeasureTheory.aestatement and proof · cited by 2,352
ENorm.enormstatement and proof · cited by 715
Filter.Eventually.monoproof · cited by 646

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_topproof · cited by 1