FarPolicyScales.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The recursive split supplies the far-branch scale conditions

The estimates use the actual largest remaining descriptor length. The angular multiplier scale is one, which is preserved by the normalized inverse construction. All constants are chosen before the terminal depth.

def OAI.Falconer.descriptorListScale line 16
theorem OAI.Falconer.eventual_descriptor_list_scale line 20

theorem OAI.Falconer.eventual_far_split_scales line 51

Source documentation

Every geometric frequency condition in JetStateFarData follows from the split gap and the largest descriptor length.

theorem eventual_far_split_scales (d : ℕ) {σ : ℝ}
    (hσ : 0 < σ) (hσ1 : σ ≤ 1) :
    ∃ N₀ : ℕ, ∀ N ≥ N₀, ∀ L h t : ℕ, L ≤ N → h ≤ t →
      20*σ*(N:ℝ) ≤ (t:ℝ)-h → 2*(L:ℝ) ≤ (t:ℝ)-h →
      ∀ D : ℝ, 1 ≤ D → D ≤ descriptorDerivativeScale N σ L →
      h+6 ≤ t ∧ D ≤ ((2:ℝ)^N)^2 ∧
      D^2 ≤ (2:ℝ)^((t:ℝ)-(h+6:ℕ)) ∧
      D^2 ≤ (2:ℝ)^t*farMinimumLength d h ∧
      ((2:ℝ)^N)^(16*σ) ≤ (2:ℝ)^t*farMinimumLength d h ∧
      1 ≤ ((2:ℝ)^t/4)*farMinimumLength d h ∧
      D^2/(((2:ℝ)^t/4)*farMinimumLength d h) ≤ ((2:ℝ)^N)^(-16*σ) := by
…

Mentions: OAI.Falconer.descriptorDerivativeScale, OAI.Falconer.farMinimumLength