OAI/NumberTheory/Ostmann/Construction/InitialMovingAverage.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.initialMovingRegularPrior line 9
2. theorem OAI.Ostmann.initial_retained_prior line 14
3. theorem OAI.Ostmann.initial_sum_prior_split line 25
4. theorem OAI.Ostmann.initial_retained_average line 41
5. def OAI.Ostmann.initialGiantAssignment line 66
6. theorem OAI.Ostmann.initial_bool_prior_average line 72
7. theorem OAI.Ostmann.initialFrozenAmplitude_movingOrder line 86
8. theorem OAI.Ostmann.initialFrozenAmplitude_moving line 111

   Source documentation

   Both original giants and all regular marginals keep their exact laws.

   theorem initialFrozenAmplitude_moving (P : Finset ℕ) [∀ p : P, NeZero (p : ℕ)]
       (b d r : ℕ) (μg : P → ℝ) (μb : Fin b → P → ℝ) (μc : Fin r → P → ℝ)
       (F : Fin ((b + (d + r) + 1) + (b + (d + r) + 1)) → (p : P) → ZMod (p : ℕ) → ℂ)
       (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (V : ℕ)
       (w : (Fin ((b + (d + r) + 1) + (b + (d + r) + 1)) → P) → ℂ)
       (sl sr : Fin d → P) :
       initialFrozenAmplitude P b d r μg μb μc F ψ X V w sl sr =
         ∑ XL : P, (μg XL : ℂ) * ∑ XR : P, (μg XR : ℂ) *
           ∑ y : MovingRegularSlot 0 (r + r) (b + b) → P,
             ((∏ i, initialMovingRegularPrior b r μb μc i (y i) : ℝ) : ℂ) *
               let x := initialMovingTuple b d r sl sr XL XR y
   …

   Mentions: OAI.Ostmann.initialFrozenAmplitude, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.initialMovingRegularPrior, OAI.Ostmann.initialMovingTuple