Core

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

Deterministic recurrence integration: local estimates

This file contains the exact scalar increment/comparator objects and Steps 1--2 of ABK26 l.integrate.approx.recurrence. It is purely deterministic. The recurrence increment and comparator use the directional cstar; the Frobenius envelope constant does not enter these local estimates.

The geometric-sum identities are consumed from the current public Provider.Stream.GeometricSums A.

References

• ABK26.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.geometricTerm (gamma : ℝ) (k : ℤ) : ℝ

The geometric term 3^(2 gamma k) used throughout the recurrence.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.geometricTerm gamma k = 3 ^ (2 * gamma * ↑k)

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.recurrenceIncrement (cstar gamma : ℝ) (n m : ℤ) : ℝ

The directional increment A_{n,m} from e.A.def.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.recurrenceIncrement cstar gamma n m = cstar * Real.log 3 * ∑ k ∈ Finset.Icc (n + 1) m, 3 ^ (2 * gamma * ↑k)

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.recurrenceComparator (nu cstar gamma : ℝ) (m : ℤ) : ℝ

The exact-increment comparator T_m.

Equations

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

@[simp]

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.geometricTerm_pos (gamma : ℝ) (k : ℤ) : 0 < geometricTerm gamma k

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.recurrenceComparator_sub_eq_two_increment {nu cstar gamma : ℝ} (hgamma : 0 < gamma) {n m : ℤ} (hnm : n ≤ m) : recurrenceComparator nu cstar gamma m - recurrenceComparator nu cstar gamma n = 2 * recurrenceIncrement cstar gamma n m

The exact comparator increment T_m - T_n = 2 A_{n,m}.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.log_three_le_two : Real.log 3 ≤ 2

A crude bound used in Step 2.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.square_increment_upper {x y yi ε A D : ℝ} (hx : 0 < x) (hy : 0 < y) (hyi : 0 < yi) (hyyi : y * yi = 1) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hA : 0 ≤ A) (hD : 0 ≤ D) (hu : x ≤ (1 + ε) * y + A * yi) : x ^ 2 - y ^ 2 - 2 * A ≤ (3 * ε + (A * yi ^ 2) ^ 2 + 2 * D) * (y ^ 2 + 2 * A)

Upper half of e.local.square.increments: x² − y² − 2A ≤ (3ε + (A yi²)² + 2D)(y² + 2A). Obtained by squaring the upper recurrence bound.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.square_increment_lower_strong {x y yi ε A D : ℝ} (hx : 0 < x) (hy : 0 < y) (_hyi : 0 < yi) (hyyi : y * yi = 1) (hε0 : 0 ≤ ε) (hε1 : ε < 1) (hA : 0 ≤ A) (hD : 0 ≤ D) (hl : (1 - ε) * y ≤ (1 - A * yi ^ 2 + D) * x) : -(2 * (ε + D) * (y ^ 2 + 2 * A)) ≤ x ^ 2 - y ^ 2 - 2 * A

Lower half of e.local.square.increments: x² − y² − 2A ≥ −2(ε + D)(y² + 2A), obtained by squaring the lower recurrence bound and the elementary inequality (1−u)⁻² ≥ 1 + 2u (equivalently (1+2u)(1−u)² ≤ 1 for u < 1) with u = A yi² − D.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.double_local_square_increment {x y yi ε A D : ℝ} (hx : 0 < x) (hy : 0 < y) (hyi : 0 < yi) (hyyi : y * yi = 1) (hε0 : 0 ≤ ε) (hε1 : ε < 1) (hA : 0 ≤ A) (hD : 0 ≤ D) (hu : x ≤ (1 + ε) * y + A * yi) (hl : (1 - ε) * y ≤ (1 - A * yi ^ 2 + D) * x) : |x ^ 2 - y ^ 2 - 2 * A| ≤ (3 * ε + (A * yi ^ 2) ^ 2 + 2 * D) * (y ^ 2 + 2 * A)

e.double.local.square.increment: the two-sided bound on the squared increment.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.geometricTerm_mono {γ : ℝ} (hγ : 0 < γ) {k l : ℤ} (hkl : k ≤ l) : geometricTerm γ k ≤ geometricTerm γ l

k ↦ 3^{2γk} is monotone for γ > 0.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.geometricTerm_ratio_le {γ : ℝ} (hγ : 0 < γ) {n m : ℤ} (hrange : ↑m ≤ ↑n + γ⁻¹) : geometricTerm γ m ≤ 9 * geometricTerm γ n

On a unit gamma⁻¹ step, 3^{2γm} ≤ 9·3^{2γn}.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.recurrenceIncrement_nonneg {cstar γ : ℝ} (hcstar : 0 ≤ cstar) (n m : ℤ) : 0 ≤ recurrenceIncrement cstar γ n m

A_{n,m} ≥ 0.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.recurrenceIncrement_le_count {cstar γ : ℝ} (hγ : 0 < γ) (hcstar : 0 ≤ cstar) {n m : ℤ} (hnm : n ≤ m) : recurrenceIncrement cstar γ n m ≤ cstar * Real.log 3 * (↑m - ↑n) * geometricTerm γ m

A_{n,m} ≤ c⋆ (log 3)(m−n) 3^{2γm} (each of the m−n terms is ≤ 3^{2γm}).

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.nu_sq_le_recurrenceComparator {ν cstar γ : ℝ} (hcstar : 0 ≤ cstar) (hγ : 0 < γ) (n : ℤ) : ν ^ 2 ≤ recurrenceComparator ν cstar γ n

T_n ≥ ν².

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.cstar_geometricTerm_le_recurrenceComparator {ν cstar γ : ℝ} (_hν : 0 < ν) (hcstar : 0 ≤ cstar) (hγ : 0 < γ) (n : ℤ) : cstar * γ⁻¹ * geometricTerm γ n ≤ recurrenceComparator ν cstar γ n

T_n ≥ c⋆ γ⁻¹ 3^{2γn} (from K_γ ≥ γ⁻¹).

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.two_recurrenceIncrement_min_bound {ν cstar γ : ℝ} (hν : 0 < ν) (hcstar : 0 < cstar) (hγ : 0 < γ) {n m : ℤ} (hnm : n ≤ m) (hrange : ↑m ≤ ↑n + γ⁻¹) : 2 * recurrenceIncrement cstar γ n m ≤ 40 * min ((ν ^ 2)⁻¹ * cstar * geometricTerm γ n) γ * (↑m - ↑n) * recurrenceComparator ν cstar γ n

e.chunk display: 2 A_{n,m} ≤ 40 · min{ν⁻²c⋆3^{2γn}, γ} · (m−n) · T_n.

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.cstar_geometricTerm_min_bound {ν cstar γ : ℝ} (hν : 0 < ν) (hcstar : 0 < cstar) (hγ : 0 < γ) {n m : ℤ} (_hnm : n ≤ m) (hrange : ↑m ≤ ↑n + γ⁻¹) : cstar * geometricTerm γ m ≤ 9 * min ((ν ^ 2)⁻¹ * cstar * geometricTerm γ n) γ * recurrenceComparator ν cstar γ n

e.chunk display: c⋆ 3^{2γm} ≤ 9 · min{ν⁻²c⋆3^{2γn}, γ} · T_n (the paper's T_n⁻¹3^{2γm} ≤ C c⋆⁻¹ min{…} in division-free form).

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.geometricTerm_two_gamma (γ : ℝ) (m : ℤ) : geometricTerm (2 * γ) m = geometricTerm γ m ^ 2

3^{4γm} = (3^{2γm})².

theorem Algsuperdiff.Section3.Provider.Diffusivity.RecurrenceIntegration.Internal.chunk_increment_under_sass {ν cstar γ E F : ℝ} {m₀ : ℤ} {s : ℤ → ℝ} (hν : 0 < ν) (hcstar : 0 < cstar) (hγ : 0 < γ) (hE : 1 ≤ E) (hF : 1 ≤ F) (hpos : ∀ (k : ℤ), 0 < s k) (hEγ : E * γ < 1) (hupper : ∀ (a b : ℤ), b ≤ m₀ → a ≤ b → ↑b ≤ ↑a + cstar * γ⁻¹ → s b ≤ (1 + E * γ) * s a + recurrenceIncrement cstar γ a b * (s a)⁻¹) (hlower : ∀ (a b : ℤ), b ≤ m₀ → a ≤ b → ↑b ≤ ↑a + cstar * γ⁻¹ → (1 - E * γ) * s a + recurrenceIncrement cstar γ a b * (s a)⁻¹ ^ 2 * s b - F * (↑b - ↑a) ^ 2 * (s a)⁻¹ ^ 4 * s b * geometricTerm (2 * γ) b ≤ s b) {n m : ℤ} (hm₀ : m ≤ m₀) (hnm : n ≤ m) (hsourceRange : ↑m ≤ ↑n + cstar * γ⁻¹) (hunitRange : ↑m ≤ ↑n + γ⁻¹) (hsass_lo : 1 / 2 * recurrenceComparator ν cstar γ n ≤ s n ^ 2) (hsass_hi : s n ^ 2 ≤ 2 * recurrenceComparator ν cstar γ n) : |s m ^ 2 - s n ^ 2 - 2 * recurrenceIncrement cstar γ n m| ≤ 3200 * γ * (E + (1 + (cstar ^ 2)⁻¹ * F) * min ((ν ^ 2)⁻¹ * cstar * γ⁻¹ * geometricTerm γ n) 1 ^ 2 * γ * (↑m - ↑n) ^ 2) * recurrenceComparator ν cstar γ m

e.chunk.increment.under.sass.