OAI/Analysis/LipschitzHilbert/Trees/SourceCentralPowerGain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The numerical gain in manuscript §11, with the actual rounded number of shifts. A polynomial separated-count bound gives the required phase lower bound, and the central exponent absorbs every fixed power of L.

  1. theorem OAI.LipschitzHilbert.eventually_phaseParameter_lower line 16
  2. theorem OAI.LipschitzHilbert.central_exponent_gap line 37
  3. theorem OAI.LipschitzHilbert.eventually_source_central_power_gain line 63
  4. theorem OAI.LipschitzHilbert.eventually_source_central_power_gain_actual line 111

    Source documentation

    The manuscript's rounded shift count satisfies the numerical hypothesis without replacing it by an unrounded real parameter.

    theorem eventually_source_central_power_gain_actual (d C Q : ℝ)
    (hd : 0 ≤ d) (hC : 0 ≤ C) (hQ : 0 ≤ Q) :
    ∀ᶠ L : ℝ in atTop, ∀ D N : ℝ,
      1 ≤ D → D ≤ L^d → 0 < N → L/2 ≤ Real.log N →
      L^C*N^(1-phaseParameter D/Real.sqrt L+
        ((1+phaseParameter D)/Real.sqrt L)/(SourceParameters.blockCount L:ℝ)) ≤
        L^(-Q)*N := by
…

    Mentions: OAI.LipschitzHilbert.SourceParameters.blockCount