OAI/NumberTheory/Ostmann/Characters/PivotLossBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual factorial and harmonic-mass loss in the transfer iteration

  1. def OAI.Ostmann.pivotLogLoss line 13
  2. theorem OAI.Ostmann.pivotLogLoss_nonneg line 16
  3. theorem OAI.Ostmann.harmonic_pivot_loss_le line 22
  4. theorem OAI.Ostmann.eventual_pivot_loss_budget line 40

    Source documentation

    For fixed depth the factorial terms are constants in L. The selected cell-role budget leaves enough room for all Cauchy losses and floor rounding.

    theorem eventual_pivot_loss_budget (k : ℕ) (r : Fin k → ℕ) (C z : ℝ)
    (hC : 0 ≤ C) (hz : 0 < z) (hsmall : C * (∑ j, (r j : ℝ)) ≤ z / 4) :
    ∀ᶠ L : ℝ in atTop,
      (∀ j, 0 ≤ pivotLogLoss (r j) C L) ∧
      (∑ j, (pivotLogLoss (r j) C L + Real.log 2)) ≤ (⌊z * L⌋₊ : ℝ) := by
…

    Mentions: OAI.Ostmann.pivotLogLoss