OAI/NumberTheory/Ostmann/Arithmetic/MovingAmplitudeEnergyLogNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingAmplitudeRegularEnergy_bulk_log_le line 13

   Source documentation

   This comparison is applied after the harmonic diagonal reduction. The signed two-branch comparison keeps the log weights throughout.

   theorem movingAmplitudeRegularEnergy_bulk_log_le
       (P Pg I : Finset ℕ) (tier : P → ℕ) (k : ℕ)
       (outside : List ℕ) (cb cd : ℝ) (μ : ℕ → P → ℝ)
       (hμ0 : ∀ j a, 0 ≤ μ j a) (hμ : ∀ j a, μ j a ≠ 0 → tier a = j)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState P → ℤ → ℂ)
       (φ : ℝ → ℝ) (hφ : ∀ x, 0 ≤ φ x) (G : ℕ → ℝ)
       (n r m : ℕ) (hn : n < k) (Q : MovingRegularSlot n r m → Finset ℕ)
       (hsmall : ∀ j : TreeLeafIndex n × Fin r, ∀ q : P,
         primeSubsetPrior P (Q (j.1, .inl j.2)) q ≠ 0 → tier q ≠ k)
       (hbulk : ∀ j : TreeLeafIndex n × Fin m, ∀ q : P,
         primeSubsetPrior P (Q (j.1, .inr j.2)) q ≠ 0 → tier q = k)
       (greg : ∀ q : ℕ, ZMod q → ℂ) :
   …

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

2. theorem OAI.Ostmann.movingAmplitude_harmonic_unweighted_cost_le line 60

   Source documentation

   The full diagonal reduces to the original one-branch energy with its explicit counterpart cost.

   theorem movingAmplitude_harmonic_unweighted_cost_le
       (P Pg I : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hPg : ∀ p ∈ Pg, p.Prime)
       (tier : P → ℕ) (k : ℕ) (outside : List ℕ) (cb cd : ℝ)
       (μ : ℕ → P → ℝ) (hμ0 : ∀ j a, 0 ≤ μ j a)
       (hμ : ∀ j a, μ j a ≠ 0 → tier a = j)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState P → ℤ → ℂ)
       (hF : ∀ x, F x 0 = 0)
       (φ : ℝ → ℝ) (hφ0 : ∀ x, 0 ≤ φ x) (hφ1 : ∀ x, φ x ≤ 1) (G : ℕ → ℝ)
       (n r m : ℕ) (hn : n < k) (Q : MovingRegularSlot n r m → Finset ℕ)
       (hsmall : ∀ j : TreeLeafIndex n × Fin r, ∀ q : P,
         primeSubsetPrior P (Q (j.1, .inl j.2)) q ≠ 0 → tier q ≠ k)
       (hbulk : ∀ j : TreeLeafIndex n × Fin m, ∀ q : P,
   …

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