OAI/NumberTheory/Ostmann/Arithmetic/MovingAmplitudeMaskedEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.amplitude_energy_fubini line 12

   Also declared: OAI/NumberTheory/Ostmann/Arithmetic/MovingAmplitudeSymmetrizedMasked.lean:12 (same declaration text).

2. theorem OAI.Ostmann.movingAmplitudeRegularEnergy_fubini line 39

   Source documentation

   The compensation draw and the surviving draw are independent original priors; this reordering introduces no frequency probability factor.

   theorem movingAmplitudeRegularEnergy_fubini
       (P Pg I : Finset ℕ) (outside : List ℕ) (μ : ℕ → P → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState P → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ)
       (Q : MovingRegularSlot n r m → Finset ℕ) (greg : ∀ q : ℕ, ZMod q → ℂ) :
       movingAmplitudeRegularEnergy P Pg I outside μ childBound pivotBound V F φ G n r m Q greg =
       ∑ u : TreeLeafIndex n × Fin 4 → P, (∏ i, μ n (u i)) * (∏ i, (u i : ℕ) : ℕ) *
         ∑ y : MovingRegularSlot n r m → P, (∏ i, primeSubsetPrior P (Q i) (y i)) *
           ∑ p ∈ I, φ (Real.log p - G (n + 1)) *
             ∑ X : Pg, smoothGiantPrior Pg φ (G (n + 1)) X *
               ∑ s : transferFrequencyRange (V n),
                 ‖movingTemplateCoefficient Subtype.val outside μ childBound pivotBound V F φ G
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingAmplitudeRegularEnergy, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.smoothGiantPrior, OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.movingTemplateCoefficient

3. theorem OAI.Ostmann.movingAmplitudeRegularEnergy_eq_masked line 73

   Source documentation

   This is the literal arithmetic energy under the original restored prior. The extracted compensation product is a weight, not a change of measure.

   theorem movingAmplitudeRegularEnergy_eq_masked
       (P Pg I : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (outside : List ℕ) (μ : ℕ → P → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState P → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ)
       (Q : MovingRegularSlot n r m → Finset ℕ) (greg : ∀ q : ℕ, ZMod q → ℂ) :
       movingAmplitudeRegularEnergy P Pg I outside μ childBound pivotBound V F φ G n r m Q greg =
         movingMaskedTemplateEnergy P Pg I hP outside μ childBound pivotBound V F φ G n r m Q greg
           (fun x => (movingRestoredCompensationProduct Subtype.val n r m x : ℝ)) := by
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingAmplitudeRegularEnergy, OAI.Ostmann.movingMaskedTemplateEnergy, OAI.Ostmann.movingRestoredCompensationProduct

4. theorem OAI.Ostmann.movingAmplitudeRegularEnergy_le_masked line 100

   Source documentation

   The compensation cost is now explicit, with the same original prior in both energies. The bound is used only after the nonnegative diagonal reduction.

   theorem movingAmplitudeRegularEnergy_le_masked
       (P Pg I : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (outside : List ℕ) (μ : ℕ → P → ℝ)
       (hμ : ∀ j a, 0 ≤ μ j a)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState P → ℤ → ℂ)
       (φ : ℝ → ℝ) (hφ : ∀ t, 0 ≤ φ t) (G : ℕ → ℝ) (n r m : ℕ)
       (Q : MovingRegularSlot n r m → Finset ℕ) (greg : ∀ q : ℕ, ZMod q → ℂ)
       (b : ℝ) (hb : ∀ a, μ n a ≠ 0 → (a : ℝ) ≤ Real.exp b) :
       movingAmplitudeRegularEnergy P Pg I outside μ childBound pivotBound V F φ G n r m Q greg ≤
         Real.exp (((2 ^ n * 4 : ℕ) : ℝ) * b) *
           movingMaskedTemplateEnergy P Pg I hP outside μ childBound pivotBound V F φ G n r m Q greg
             (fun _ => 1) := by
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingAmplitudeRegularEnergy, OAI.Ostmann.movingMaskedTemplateEnergy