OAI/NumberTheory/Ostmann/Arithmetic/MovingInternalFiber.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingInternalPairFactor_fiber line 12
2. theorem OAI.Ostmann.movingInternalPairFactor_fiber_error line 43

   Source documentation

   The square loss is relative to the base line event. The number of forbidden zero lifts is bounded by the number of nodes in the two histories.

   theorem movingInternalPairFactor_fiber_error {σ : Type*} {n : ℕ}
       (tier : σ → ℕ) (value : σ → ℕ) (hprime : ∀ i, (value i).Prime)
       (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
       (T : Bool → MovingSlotData σ n) (hlevels : ∀ side, (T side).Levels tier)
       (p : ℕ) [Fact p.Prime]
       (hf : ∀ side, (T side).Frequencies (fun s => (s : ZMod p) ≠ 0))
       (x₀ y₀ : ZMod p) (hy : y₀ ≠ 0)
       (hbase : ∀ j : MovingPrimeOccurrences value T p,
         let φ := MovingSlotReversal.naturalReduction p value
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingPrimeOccurrences, OAI.Ostmann.MovingSlotReversal.naturalReduction