OAI/NumberTheory/Ostmann/Construction/SmoothGiantPrior.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.smoothGiantMass line 10
2. def OAI.Ostmann.smoothGiantLogNormalizer line 13
3. def OAI.Ostmann.smoothGiantPrior line 16
4. theorem OAI.Ostmann.smoothGiantPrior_nonneg line 19
5. theorem OAI.Ostmann.smoothGiantPrior_mass line 23
6. theorem OAI.Ostmann.smoothGiantPrior_cancel_prime line 34

   Source documentation

   This is exactly p μ_G(p) = exp(c_g) φ(log p - G), with the normalizing constant computed from the finite original prime support.

   theorem smoothGiantPrior_cancel_prime (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (φ : ℝ → ℝ) (G : ℝ) (p : P) :
       (p : ℝ) * smoothGiantPrior P φ G p =
         Real.exp (smoothGiantLogNormalizer P φ G) * φ (Real.log p - G) := by
   …

   Mentions: OAI.Ostmann.smoothGiantPrior, OAI.Ostmann.smoothGiantLogNormalizer

7. theorem OAI.Ostmann.smoothGiantPrior_row_transfer line 43

   Source documentation

   Equation (7.12) with the actual normalized smooth prior.

   theorem smoothGiantPrior_row_transfer {A : Type*} [Fintype A]
       (P I : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hPI : P ⊆ I)
       (φ : ℝ → ℝ) (G : ℝ) (hφ : ∀ x, 0 ≤ φ x)
       (hpos : 0 < smoothGiantMass P φ G)
       (μ : A → ℝ) (hμ : ∀ a, 0 ≤ μ a) (hμmass : ∑ a, μ a = 1)
       (U : A → ℕ)
       (row : ∀ a, (p : P) → Fin ((p : ℕ) * U a) → ℂ)
       (B : ∀ a p, Fin (p * U a) → ℂ)
       (hrow : ∀ a p, (∑ t, ‖row a p t‖ ^ 2) ≤ (p : ℕ) * (U a : ℝ)) :
       ‖∑ a, (μ a : ℂ) * ∑ p : P, (smoothGiantPrior P φ G p : ℂ) *
           ∑ t, row a p t * B a p t‖ ^ 2 ≤
         Real.exp (smoothGiantLogNormalizer P φ G) *
   …

   Mentions: OAI.Ostmann.smoothGiantMass, OAI.Ostmann.smoothGiantPrior, OAI.Ostmann.smoothGiantLogNormalizer