OAI/NumberTheory/Ostmann/Characters/CharacterAtomIteration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Iteration with the selected word bin and actual character cell products

  1. def OAI.Ostmann.characterPivotRole line 14
  2. theorem OAI.Ostmann.characterPivotRole_eq line 17
  3. def OAI.Ostmann.characterPivotCap line 21
  4. theorem OAI.Ostmann.characterPivotCap_eq line 24
  5. theorem OAI.Ostmann.eventual_character_atom_iteration line 31

    Source documentation

    The transfer geometry and all pivot losses are derived from the chosen cell endpoints. The remaining diagonal premise is the literal matching sum estimated separately by the selected-bulk energy and cancellation theorems.

    theorem eventual_character_atom_iteration (k : ℕ) (r : Fin k → ℕ) (f : ℕ)
    (hr : ∀ j, 0 < r j) (B B₀ z c Cmass : ℝ)
    (hB : 0 ≤ B) (hz : 1 ≤ z) (hc : 1 ≤ c) (hCmass : 0 ≤ Cmass)
    (hbudget : Cmass * (∑ j, (r j : ℝ)) ≤ z / 4) :
    ∀ᶠ L : ℝ in atTop,
    let m := ⌊z * L⌋₊
…