SourceReferenceThreshold.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Fixed binary reference grids give polynomial thresholds with arbitrarily strong exponential tails. The angular grid branching never enters this bound.

theorem OAI.LipschitzHilbert.SourceLatticePacket.binary_lineMomentBase_le line 16
Source documentation
The reference variation constant grows at most linearly with the packet envelope constant. All other parameters precede the packet family.
```
theorem binary_lineMomentBase_le (M B C : ℝ) (hM : 0 ≤ M) (hB : 0 ≤ B)
    (hC : 0 ≤ C) :
    lineMomentBase C (M*C^2*B+1) 2 ≤
      lineMomentBase 1 (M*B+1) 2*(C+1) := by
…
```
Mentions: OAI.LipschitzHilbert.lineMomentBase

theorem OAI.LipschitzHilbert.SourceLatticePacket.eventually_reference_thresholds line 42

Source documentation

One natural moment order works for every reference packet family, line position, and binary grid. Its threshold is a fixed power of L.

theorem eventually_reference_thresholds (M B a J : ℝ)
    (hM : 0 ≤ M) (hB : 0 ≤ B) (ha : 0 ≤ a) (hJ : 0 ≤ J) :
    ∀ᶠ L : ℝ in atTop, ∃ n : ℕ, 1 ≤ n ∧
      (1/4:ℝ)^n ≤ Real.exp (-J*L) ∧ 1 ≤ L^(a+4) ∧
      ∀ (grid : FiniteLineGrid) (C : ℝ), grid.branching = 2 →
        0 ≤ C → C ≤ L^a →
        4*(referenceSquareMomentBase B grid*(n:ℝ)) ≤ L^(a+4) ∧
        4*(lineMomentBase C (M*C^2*B+1) grid.branching*(n:ℝ)) ≤ L^(a+4) := by
…

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

theorem OAI.LipschitzHilbert.SourceLatticePacket.reference_polynomial_tails_of_moments line 102

Source documentation

The moment hypotheses are the exact previously proved reference moment bounds; no concentration or path estimate is assumed.

theorem reference_polynomial_tails_of_moments {X : Type*} [MeasurableSpace X]
    (μ : Measure X) (F V : X → ℝ) (hF : Measurable F) (hV : Measurable V)
    (M B C T : ℝ) (grid : FiniteLineGrid) (hB : 0 ≤ B) (hC : 0 ≤ C)
    (n : ℕ) (hn : 1 ≤ n) (hT : 1 ≤ T)
    (hs : 4*(referenceSquareMomentBase B grid*(n:ℝ)) ≤ T)
    (hv : 4*(lineMomentBase C (M*C^2*B+1) grid.branching*(n:ℝ)) ≤ T)
    (hsm : (∫⁻ x, (ENNReal.ofReal |F x|)^(2*(n:ℝ)) ∂μ) ≤
      referenceSquareMomentCost B grid (2*(n:ℝ))*μ univ)
    (hvm : (∫⁻ x, (ENNReal.ofReal |V x|)^(n:ℝ) ∂μ) ≤
      referenceVariationMomentCost M C B grid n*μ univ) :
    μ {x | T ≤ |F x|} ≤ (1/4:ℝ≥0∞)^n*μ univ ∧
      μ {x | T ≤ |V x|} ≤ (1/4:ℝ≥0∞)^n*μ univ := by
…

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