ScaledConcentration.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Coarse-band violations survive the small diagonal enlargement and are therefore bounded by Ford's published coordinate concentration.

lemma OAI.TotientAsymptotic.rescaled_band_violation line 15
lemma OAI.TotientAsymptotic.volume_scaled_set_le line 29
lemma OAI.TotientAsymptotic.measurableSet_coarseCoordinateBad line 48

theorem OAI.TotientAsymptotic.scaled_coarse_concentration line 55

Source documentation

The concentration bound after diagonal normalization, before summing retained coordinates. All scale and center comparisons are explicit.

theorem scaled_coarse_concentration (hford : FordCoordinateConcentrationInput) :
    ∃ C c : ℝ, ∃ N₀ : ℕ, 0 < C ∧ 0 < c ∧
    ∀ N ≥ N₀, ∀ (m q : ℕ) (B : ℝ), 0 < B → m-q=N+2 →
    ∀ (β₀ : ℝ) (β κ : Fin (N+2) → ℝ), 0 < β₀ →
      (∀ j, 0 < β j) → (∀ j, 0 < κ j) → (∀ j, β₀ ≤ κ j) →
      (∀ i j, i < j → β i*κ i ≤ κ j) →
    ∀ (i : Fin (N+2)) (t : ℝ), i.val < N → 100*q ≤ m-(i.val+1) →
      (99/100 : ℝ)*fullSimplexCenter m B (i.val+1) ≤ t →
      t ≤ (101/100 : ℝ)*fullSimplexCenter m B (i.val+1) →
      1 ≤ κ i → κ i ≤ (102/100 : ℝ) →
      volume.real (enlargedSimplex (N+2) B β₀ β ∩
        {u | u i < (91/100 : ℝ)*t ∨ (109/100 : ℝ)*t < u i}) ≤
…

Mentions: OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.fullSimplexCenter, OAI.TotientAsymptotic.enlargedSimplex