OAI/NumberTheory/Ostmann/Arithmetic/MovingPairSquareLoss.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingInternalPairFactor_on_fiber line 11
2. theorem OAI.Ostmann.moving_internal_pair_fiber_product line 41
3. theorem OAI.Ostmann.moving_pair_joint_square_loss line 77

   Source documentation

   The two-history loss counts each node once even if it contains several copies of the same prime. All its nonzero-row assumptions are derived.

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

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