OAI/NumberTheory/Ostmann/Arithmetic/MovingRealCells.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingRealPair line 11
2. theorem OAI.Ostmann.movingRealPair_update line 14
3. def OAI.Ostmann.movingCoordinateLeft line 19
4. def OAI.Ostmann.movingCoordinateRight line 22
5. theorem OAI.Ostmann.movingCoordinate_eval line 25
6. def OAI.Ostmann.movingRealGateWeight line 30
7. theorem OAI.Ostmann.movingRealGateWeight_norm line 35
8. def OAI.Ostmann.movingRealRootCuts line 41
9. theorem OAI.Ostmann.movingArchimedeanRootCuts_card line 48
10. theorem OAI.Ostmann.movingRealRootCuts_card line 55
11. theorem OAI.Ostmann.movingRealGateWeight_rootCell line 90

    Source documentation

    These cells depend on the real fixed giant, never on residue representatives.

    theorem movingRealGateWeight_rootCell {σ : Type*} (value : σ → ℕ) {n : ℕ}
        (T : MovingSlotData σ n) (nodes : List MovingFormulaNode) (X lo hi : ℝ)
        (coord : Bool) (fixed x y : ℝ) (S : Finset ℝ)
        (hS : movingRealRootCuts value T nodes X lo hi coord fixed ⊆ S)
        (hcode : rootCellCode S x = rootCellCode S y) :
        movingRealGateWeight value T nodes X lo hi (movingRealPair coord fixed x) =
          movingRealGateWeight value T nodes X lo hi (movingRealPair coord fixed y) := by
    …

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingFormulaNode, OAI.Ostmann.movingRealRootCuts, OAI.Ostmann.rootCellCode, OAI.Ostmann.movingRealGateWeight, OAI.Ostmann.movingRealPair

12. theorem OAI.Ostmann.movingSpectatorResidue_norm line 114