OAI/Analysis/LipschitzHilbert/Trees/SourceReferenceTail.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Natural-order forms of the exact reference moments. The moment grid may have fixed binary branching, independent of the source angular step.

  1. def OAI.LipschitzHilbert.SourceLatticePacket.referenceSquareMomentBase line 15
  2. theorem OAI.LipschitzHilbert.SourceLatticePacket.referenceSquareMomentBase_pos line 19
  3. theorem OAI.LipschitzHilbert.SourceLatticePacket.reference_square_moment_majorant line 28
  4. theorem OAI.LipschitzHilbert.SourceLatticePacket.reference_variation_moment_majorant line 42
  5. theorem OAI.LipschitzHilbert.SourceLatticePacket.reference_variation_tail line 49
  6. theorem OAI.LipschitzHilbert.SourceLatticePacket.reference_square_tail line 64

    Source documentation

    The square reference quantity has an exponential tail for its square; this avoids any loss from taking roots in the moment estimate.

    theorem reference_square_tail {X : Type*} [MeasurableSpace X]
    (μ : Measure X) (F : X → ℝ) (hF : Measurable F)
    (B : ℝ) (grid : FiniteLineGrid) (hB : 0 ≤ B) (n : ℕ) (hn : 1 ≤ n)
    (hm : (∫⁻ x, (ENNReal.ofReal |F x|)^(2*(n:ℝ)) ∂μ) ≤
      referenceSquareMomentCost B grid (2*(n:ℝ))*μ univ) :
    μ {x | 4*(referenceSquareMomentBase B grid*(n:ℝ)) ≤ (F x)^2} ≤
      (1/4:ℝ≥0∞)^n*μ univ := by
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.SourceLatticePacket.referenceSquareMomentCost, OAI.LipschitzHilbert.SourceLatticePacket.referenceSquareMomentBase