OAI/Analysis/LipschitzHilbert/Trees/SourceMonotoneMaximal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Passing from finite scale cutoffs to a genuine countable maximal function. The real-valued representative is defined even on the null set where the extended supremum is infinite.

  1. def OAI.LipschitzHilbert.maximalSquare line 14
  2. def OAI.LipschitzHilbert.monotoneMaximal line 17
  3. theorem OAI.LipschitzHilbert.maximalSquare_measurable line 20
  4. theorem OAI.LipschitzHilbert.monotoneMaximal_measurable line 25
  5. theorem OAI.LipschitzHilbert.monotoneMaximal_energy line 32

    Source documentation

    A nonnegative increasing sequence with a uniform squared-integral bound has a measurable L² majorant with the same bound.

    theorem monotoneMaximal_energy {X : Type*} [MeasurableSpace X]
    (μ : Measure X) (F : ℕ → X → ℝ) (C : ℝ) (hC : 0≤C)
    (hF : ∀ n, Measurable (F n)) (hpos : ∀ n x, 0≤F n x)
    (hmono : Monotone F) (hLp : ∀ n, MemLp (F n) 2 μ)
    (henergy : ∀ n, (∫ x, (F n x)^2 ∂μ)≤C) :
    MemLp (monotoneMaximal F) 2 μ ∧
    (∫ x, (monotoneMaximal F x)^2 ∂μ)≤C ∧
    ∀ᵐ x ∂μ, ∀ n, F n x≤monotoneMaximal F x := by
…

    Mentions: OAI.LipschitzHilbert.monotoneMaximal