Theorems · Theorem · functional analysis

lp.norm_le_of_tendsto

∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {ι : Type u_5}
  {l : Filter ι} [l.NeBot] [_i : Fact (1 ≤ p)] {C : ℝ} {F : ι → ↥(lp E p)},
  (∀ᶠ (k : ι) in l, ‖F k‖ ≤ C) → ∀ {f : ↥(lp E p)}, Filter.Tendsto (id fun i => ↑(F i)) l (nhds ↑f) → ‖f‖ ≤ C

"Semicontinuity of the lp norm": If all sufficiently large elements of a sequence in lp E p have lp norm ≤ C, then the pointwise limit, if it exists, also has lp norm ≤ C.

Defined in

Mathlib.Analysis.Normed.Lp.lpSpace

Cited by

1 results in Mathlib

Foundations

Depth 225 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupFilter.NeBotFact