Theorems · Theorem · functional analysis

MeasureTheory.memLp_two_iff_integrable_sq_norm

∀ {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  {f : α → F},
  MeasureTheory.AEStronglyMeasurable f μ → (MeasureTheory.MemLp f 2 μ ↔ MeasureTheory.Integrable (fun x => ‖f x‖ ^ 2) μ)

Defined in: Mathlib.MeasureTheory.Function.L2Space
Cited by: 1 results in Mathlib
Foundations: Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites20

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

Realstatement and proof · cited by 25,697
TopologicalSpaceproof · cited by 24,529
NormedAddCommGroupstatement and proof · cited by 15,752
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Norm.normstatement and proof · cited by 5,413
MeasureTheory.Integrablestatement · cited by 1,367
ENNReal.toRealproof · cited by 859
MeasureTheory.AEStronglyMeasurablestatement and proof · cited by 755
div_eq_mul_invproof · cited by 715
MeasureTheory.MemLpstatement and proof · cited by 457

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.memLp_two_iff_integrable_sqproof · cited by 3