OAI/NumberTheory/Ostmann/Arithmetic/MovingRestoredEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingReverseTemplate_average_real line 13

   Source documentation

   Real-valued finite Fubini in exactly the restored template coordinates.

   theorem movingReverseTemplate_average_real {A : Type*} [Fintype A] (n r m : ℕ)
       (ν : MovingRegularSlot n (4 + r) m → A → ℝ)
       (F : (MovingRegularSlot n (4 + r) m → A) → ℝ) :
       (∑ x, (∏ i, ν i (x i)) * F x) =
         ∑ u : TreeLeafIndex n × Fin 4 → A,
           (∏ i, ν (movingReverseTemplate n r m (.inl i)) (u i)) *
           ∑ y : MovingRegularSlot n r m → A,
             (∏ i, ν (movingReverseTemplate n r m (.inr i)) (y i)) *
             F (movingRestoreSample n r m u y) := by
   …

   Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.movingReverseTemplate, OAI.Ostmann.movingRestoreSample

2. theorem OAI.Ostmann.movingTemplateRestoredPrior_average_real line 26

   Source documentation

   Restoring slots changes neither the compensation law nor the surviving law.

   theorem movingTemplateRestoredPrior_average_real {A : Type} [Fintype A] (n r m : ℕ)
       (μ : A → ℝ) (ν : MovingRegularSlot n r m → A → ℝ)
       (F : (MovingRegularSlot n (4 + r) m → A) → ℝ) :
       (∑ x, (∏ i, movingTemplateRestoredPrior n r m μ ν i (x i)) * F x) =
         ∑ u : TreeLeafIndex n × Fin 4 → A, (∏ i, μ (u i)) *
           ∑ y : MovingRegularSlot n r m → A, (∏ i, ν i (y i)) *
             F (movingRestoreSample n r m u y) := by
   …

   Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplateRestoredPrior, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.movingRestoreSample

3. theorem OAI.Ostmann.movingTemplateCoefficient_restored_multiplier line 39

   Source documentation

   The actual coefficient supplies the distinctness needed to replace its masked arithmetic multiplier by the surviving prime-product transform.

   theorem movingTemplateCoefficient_restored_multiplier {A : Type} [Fintype A]
       (value : A → ℕ) (hprime : ∀ a, (value a).Prime)
       (outside : List ℕ) (μ : ℕ → A → ℝ) (childBound pivotBound V : ℕ → ℕ)
       (F : MovingSlotState A → ℤ → ℂ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n r m : ℕ) (s : ℤ) (u : TreeLeafIndex n × Fin 4 → A)
       (y : MovingRegularSlot n r m → A) (XL XR : ℕ) (g : ∀ q : ℕ, ZMod q → ℂ) :
       let x := movingRestoreSample n r m u y
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingRestoreSample