GraphNormalization.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Dimension-dependent normalization and branch ledger

The critical slope is d / 2. Both copies of a profile are needed for the cancellation of the spatial normalization. The last-potential bound uses the last interval with a defined two-depth potential, even when the final interval itself is shorter.

theorem OAI.Falconer.dyadic_rpow_change_base line 18

theorem OAI.Falconer.critical_profile_normalization line 26

Source documentation

Equation rec:normalization, in every dimension.

theorem critical_profile_normalization {N : ℕ} (hN : 0 < N)
    (d a b Δ : ℝ) :
    (2 : ℝ)^(d * (b-a)) * ((2 : ℝ)^N)^(-2 * (Δ + (d/2) * (b-a) / N)) =
      ((2 : ℝ)^N)^(-2 * Δ) := by
…

theorem OAI.Falconer.two_profile_graph_normalization line 38

Source documentation

The product of split weights, child counts and prefactor ratio in graph:bound. Losses remain explicit and the two profile increments cancel the entire critical spatial exponent.

theorem two_profile_graph_normalization {N : ℕ} (hN : 0 < N)
    (d a p Δ₁ Δ₂ countLoss degree : ℝ)
    (I₁ I₂ : ℝ)
    (hI₁ : I₁ = Δ₁ + (d/2) * (p-a) / N)
    (hI₂ : I₂ = Δ₂ + (d/2) * (p-a) / N) :
    ((2 : ℝ)^N)^(-2 * (I₁+I₂)) * ((2 : ℝ)^N)^(I₁+I₂+countLoss) *
        (2 : ℝ)^(d * (p-a)) * ((2 : ℝ)^N)^degree =
      ((2 : ℝ)^N)^(-Δ₁-Δ₂+countLoss+degree) := by
…

theorem OAI.Falconer.last_potential_bound line 56

Source documentation

The last defined two-depth potential is controlled by the final start. Only the diameter Q of the two chosen nearby depths enters the loss.

theorem last_potential_bound (A : ℕ → ℝ) {u w f Q N : ℕ} {d : ℝ}
    (hQ : 0 < Q) (hwidth : u + Q ≤ w) (huf : u ≤ f) (hfw : f ≤ w)
    (hd : 0 ≤ d) (hN : 0 < N)
    (hlip : ∀ i, u ≤ i → i ≤ w →
      |A i - A f| ≤ d * |(i : ℝ) - f| / N) :
    PlanarFalconer.potential A u w Q ≤ 2 * A f + 2 * d * Q / N := by
…

Mentions: OAI.PlanarFalconer.potential

theorem OAI.Falconer.branch_exponent_of_lipschitz line 78

Source documentation

Dimension-dependent branch exponent after exact telescoping, payment of all graph costs, and the final Lipschitz potential estimate.

theorem branch_exponent_of_lipschitz (A : ℕ → ℝ) (start : ℕ → ℕ)
    (V cost loss : ℕ → ℝ) (n : ℕ) {u w Q N : ℕ} {d : ℝ}
    (terminal lossBound : ℝ)
    (hpay : ∀ k < n, V k + cost k ≤ V (k+1))
    (hloss : ∑ k ∈ Finset.range n, loss k ≤ lossBound)
    (hV : V n = PlanarFalconer.potential A u w Q)
    (hQ : 0 < Q) (hwidth : u + Q ≤ w) (huf : u ≤ start n) (hfw : start n ≤ w)
    (hd : 0 ≤ d) (hN : 0 < N)
    (hlip : ∀ i, u ≤ i → i ≤ w →
      |A i - A (start n)| ≤ d * |(i : ℝ) - start n| / N) :
    (∑ k ∈ Finset.range n,
      (-2 * (A (start (k+1)) - A (start k)) + cost k + loss k)) + terminal ≤
…

Mentions: OAI.PlanarFalconer.potential