FullBoxConcentration.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Concentration for the actual phase bands in the enlarged full simplex.

def OAI.TotientAsymptotic.fullBoxSimplex line 15
def OAI.TotientAsymptotic.phaseCoordinateBad line 19

theorem OAI.TotientAsymptotic.full_box_coordinate_concentration line 25

Source documentation

Ford concentration at the actual manuscript phase bands, with the Jacobian and truncation costs explicit.

theorem full_box_coordinate_concentration (hford : FordCoordinateConcentrationInput) :
    ∃ C c : ℝ, ∃ N₀ : ℕ, 0 < C ∧ 0 < c ∧
    ∀ {x : ℝ} {H N : ℕ}, N₀ ≤ N → 0 < B x → H ≤ m x →
      m x-P H=N+2 → P H+2 ≤ H → 100*P H ≤ H →
      Real.exp (simplexBoxTail 4 H) ≤ (102/100 : ℝ) →
      (∀ k < m x, (99/100 : ℝ)*fullSimplexCenter (m x) (B x) k ≤ bandScale x k ∧
        bandScale x k ≤ (101/100 : ℝ)*fullSimplexCenter (m x) (B x) k) →
    ∀ i : Fin (N+2), i.val < R x H →
      volume.real (fullBoxSimplex x (N+2) ∩ phaseCoordinateBad x i) ≤
        Real.exp (simplexBoxTail 4 (P H))*C*
          Real.exp (-c*(N+2-(i.val+1) : ℕ))*G x (N+2) := by
…

Mentions: OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.simplexBoxTail, OAI.TotientAsymptotic.fullSimplexCenter, OAI.TotientAsymptotic.bandScale, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.fullBoxSimplex, OAI.TotientAsymptotic.phaseCoordinateBad, OAI.TotientAsymptotic.G

def OAI.TotientAsymptotic.retainedPhaseBad line 75

theorem OAI.TotientAsymptotic.full_box_retained_concentration line 80

Source documentation

The loss for all retained coordinates is an exponential tail in H, with no growing dimension factor.

theorem full_box_retained_concentration (hford : FordCoordinateConcentrationInput) :
    ∃ C c : ℝ, ∃ N₀ : ℕ, 0 < C ∧ 0 < c ∧
    ∀ {x : ℝ} {H N : ℕ}, N₀ ≤ N → 0 < B x → H ≤ m x →
      m x-P H=N+2 → P H+2 ≤ H → 100*P H ≤ H → 2*P H ≤ H →
      Real.exp (simplexBoxTail 4 H) ≤ (102/100 : ℝ) →
      (∀ k < m x, (99/100 : ℝ)*fullSimplexCenter (m x) (B x) k ≤ bandScale x k ∧
        bandScale x k ≤ (101/100 : ℝ)*fullSimplexCenter (m x) (B x) k) →
      ∀ hRN : R x H ≤ N+2,
      volume.real (retainedPhaseBad x H (N+2) hRN) ≤
        (Real.exp (simplexBoxTail 4 (P H))*C*G x (N+2))*
          ((Real.exp (-c/2))^H/(1-Real.exp (-c/2))) := by
…