RecurrenceIntegration

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Integration of the approximate recurrence

The reported constant is one fixed numeral, independent of the sequence, of ν, c⋆, γ, E, F and of the endpoint m₀: this is the manuscript's "there exists a universal C < ∞" made explicit (see integrate_approx_recurrence_universal for the literal existential form).

No c⋆ ≤ 1

Neither the printed statement nor this formalization assumes any upper bound on c⋆: the descent instead caps its step at c = min{c⋆,1} (Internal.adaptStep_le_cap), and the resulting slack is absorbed into the single universal constant C.

References

• ABK26.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.targetProfileSq (ν cstar γ : ℝ) (m : ℤ) : ℝ

P_m = ν² + cstar γ⁻¹ 3^{2γm}, the target the conclusion compares s_m against (the √· argument in e.concl.root.gamma.inv).

Equations

• One or more equations did not get rendered due to their size.

def Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.recurrenceIntegrationConstant : ℝ

The universal constant reported by l.integrate.approx.recurrence.

Any numeral at least 2·(2·(4·recurrenceDescentConstant²)+8) = 230400000016 works: 4·recurrenceDescentConstant² is the squared-deviation constant of Internal.sq_deviation_core_explicit, the square-root reduction doubles it and adds 8 for the K_γ-versus-γ⁻¹ comparator gap, and the final factor 2 pays for rewriting the internal capped bracket in terms of the printed one. The fixed choice below is 2·(4·200000²)+8. It is independent of the sequence, of ν, c⋆, γ, E, F, and of the endpoint m₀.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.recurrenceIntegrationConstant = 320000000008

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.recurrenceIntegrationConstant_eq : recurrenceIntegrationConstant = 320000000008

The explicit numerical value of recurrenceIntegrationConstant.

l.integrate.approx.recurrence

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.integrate_approx_recurrence_cstarPlus {ν cstar cstarPlus γ E F : ℝ} {m₀ : ℤ} {s : ℤ → ℝ} (hν : 0 < ν) (hcstar : 0 < cstar) (hcstar32 : cstar ≤ 3 / 2) (hcc : cstar ≤ cstarPlus) (hγ : 0 < γ) (hE : 1 ≤ E) (hF : 1 ≤ F) (hsmall : ∀ (m : ℤ), ν ≤ s m ∧ s m ≤ (1 + (ν ^ 2)⁻¹ * cstarPlus * γ⁻¹ * 3 ^ (2 * γ * ↑m)) * ν) (hupper : ∀ (n m : ℤ), m ≤ m₀ → n ≤ m → ↑m ≤ ↑n + cstar * γ⁻¹ → s m ≤ (1 + E * γ) * s n + recurrenceIncrement cstar γ n m * (s n)⁻¹) (hlower : ∀ (n m : ℤ), m ≤ m₀ → n ≤ m → ↑m ≤ ↑n + cstar * γ⁻¹ → (1 - E * γ) * s n + recurrenceIncrement cstar γ n m * (s n)⁻¹ ^ 2 * s m - F * (↑m - ↑n) ^ 2 * (s n)⁻¹ ^ 4 * s m * 3 ^ (4 * γ * ↑m) ≤ s m) : γ ≤ (recurrenceIntegrationConstant * (E * (1 + (cstar ^ 2)⁻¹ * F + (cstar ^ 2)⁻¹ * cstarPlus)))⁻¹ → ∀ m ≤ m₀, |s m - √(ν ^ 2 + cstar * γ⁻¹ * 3 ^ (2 * γ * ↑m))| ≤ recurrenceIntegrationConstant * √(E * (1 + (cstar ^ 2)⁻¹ * F + (cstar ^ 2)⁻¹ * cstarPlus) * γ) * s m

Two-constant form of l.integrate.approx.recurrence.

The manuscript denominates both the a-priori envelope e.small.scale.bound and the fixed-point target A_{n,m} / P_m in the single constant c⋆.

Taking c⁺ = c⋆ recovers integrate_approx_recurrence up to the universal constant. This is not a node statement: l.integrate.approx.recurrence is integrate_approx_recurrence above.