CharacterDiagonalGap.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The original whole-word product pays the diagonal endpoint count

theorem OAI.Ostmann.character_diagonal_product_gap line 12

Source documentation

Extract the reciprocal H product before summing the extended pivot. The loss is only twice the fixed covering error.

theorem character_diagonal_product_gap {k n : ℕ} (hn : n < k)
    (J B z m F c : ℝ) (hc : 0 ≤ c) (a : Fin k → Bool → ℝ)
    (lo hi : CharacterRole k → ℕ)
    (hlo : ∀ i, Real.exp (characterLogCenter J
      (characterPivotTarget k J (fun j => a j false + a j true)
        (fun j => characterPivotGap B z m j.val)) a F i - c) ≤ lo i)
    (hhi : ∀ i, (hi i : ℝ) ≤ Real.exp (characterLogCenter J
      (characterPivotTarget k J (fun j => a j false + a j true)
        (fun j => characterPivotGap B z m j.val)) a F i + c)) :
    let T := characterPivotTarget k J (fun j => a j false + a j true)
…

Mentions: OAI.Ostmann.CharacterRole, OAI.Ostmann.characterLogCenter, OAI.Ostmann.characterPivotTarget, OAI.Ostmann.characterPivotGap

theorem OAI.Ostmann.character_diagonal_gap_reserve line 40

Source documentation

A fixed covering loss is absorbed by one unit of the linear gap coefficient.

theorem character_diagonal_gap_reserve (n : ℕ) (B z m C : ℝ)
    (hm : 0 ≤ m) (hC : 2 * C ≤ m) :
    (B + 20 * Real.log z - 1) * (2 ^ n : ℕ) * m ≤
      characterPivotGap B z m n - 2 * C := by
…

Mentions: OAI.Ostmann.characterPivotGap