Essential supremum

TheoremEssential supremum of a continuous map#✓fully proved

Let \(\alpha\) be a compact topological space with its Borel \(\sigma\)-algebra, let \(\mu\) be a measure on \(\alpha\) that is positive on every nonempty open set, let \(E\) be a seminormed additive commutative group, and let \(f : \alpha \to E\) be continuous. Then the essential supremum of \(\|f\|\) with respect to \(\mu\) equals the supremum norm \(\sup_{x \in \alpha} \|f(x)\|\) of \(f\), as an equality in \([0, \infty]\).

theorem eLpNormEssSup_eq_enorm_continuousMap
    {α : Type*} [TopologicalSpace α] [CompactSpace α] [MeasurableSpace α]
    [BorelSpace α] {μ : Measure α} [μ.IsOpenPosMeasure]
    {E : Type*} [SeminormedAddCommGroup E] (f : C(α, E)) :
    eLpNormEssSup (fun x => f x) μ = ‖f‖ₑ

Used by 1

Used byThe \(L^\infty\) norm of a continuous map is its supremum norm

TheoremThe \(L^\infty\) norm of a continuous map is its supremum norm#✓fully proved

Let \(\alpha\) be a compact topological space with its Borel \(\sigma\)-algebra, let \(\mu\) be a measure on \(\alpha\) that is positive on every nonempty open set, let \(E\) be a seminormed additive commutative group such that \(\alpha\) or \(E\) is second-countable, and let \(f : \alpha \to E\) be continuous. Then \(\|f\|_{L^\infty(\mu)} = \sup_{x \in \alpha} \|f(x)\|\), as an equality in \([0, \infty]\).

theorem eLpNorm_top_eq_enorm_continuousMap
    {α : Type*} [TopologicalSpace α] [CompactSpace α] [MeasurableSpace α]
    [BorelSpace α] {μ : Measure α} [μ.IsOpenPosMeasure]
    {E : Type*} [SeminormedAddCommGroup E] [SecondCountableTopologyEither α E]
    (f : C(α, E)) :
    eLpNorm (fun x => f x) ⊤ μ = ‖f‖ₑ

Uses 1

Proof usesEssential supremum of a continuous map

TheoremThe \(L^p\) norm tends to the \(L^\infty\) norm#●ready to prove

Let \(\mu\) be a finite measure on a measurable space \(\alpha\) and let \(f \colon \alpha \to \mathbb{R}\) be essentially bounded, \(f \in L^\infty(\mu)\). Then \(\|f\|_{L^p(\mu)} \to \|f\|_{L^\infty(\mu)}\) as the real exponent \(p\) tends to \(\infty\).

public theorem_wanted tendsto_eLpNorm_atTop_eLpNorm_top_of_isFiniteMeasure
    {α : Type*} [MeasurableSpace α] {μ : Measure α}
    (hmu : μ Set.univ < ∞) {f : α → ℝ} (hf : MemLp f ∞ μ) :
    Tendsto (fun p : NNReal => eLpNorm f p μ) atTop
      (𝓝 (eLpNorm f ∞ μ))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l1_42.

TheoremUniform \(L^p\) bounds on \((0,1)\) give the same \(L^\infty\) bound#●ready to prove

Let \(M\) be a real number, write \(M^+ = \max(M, 0)\), and let \(f_0, f_1, f_2, \dots : \mathbb{R} \to \mathbb{R}\) be functions that are almost everywhere strongly measurable with respect to Lebesgue measure restricted to \([0,1]\). If \(\|f_n\|_{L^p[0,1]} \le M^+\) for every \(n\) and every real \(p \ge 1\), then \(\|f_n\|_{L^\infty[0,1]} \le M^+\) for every \(n\). All norms are taken with respect to Lebesgue measure restricted to \([0,1]\) and may be infinite.

public theorem_wanted eLpNorm_top_le_of_forall_one_le_eLpNorm_le
    (f : ℕ → ℝ → ℝ) (M : ℝ)
    (hf : ∀ n : ℕ, AEStronglyMeasurable (f n) (volume.restrict (Set.Icc (0 : ℝ) 1)))
    (hM : ∀ n : ℕ, ∀ p : ℝ, 1 ≤ p →
      eLpNorm (f n) (ENNReal.ofReal p) (volume.restrict (Set.Icc (0 : ℝ) 1)) ≤ ENNReal.ofReal M) :
    ∀ n : ℕ, eLpNorm (f n) ⊤ (volume.restrict (Set.Icc (0 : ℝ) 1)) ≤ ENNReal.ofReal M

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l2_52.

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.