OAI/NumberTheory/Ostmann/Construction/SmoothGiantMixedInterval.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.smoothInteger_interval line 13

   Source documentation

   The integer coordinate has its original counting weight. Passing to the logarithmic cell introduces exactly the displayed exponential scale.

   theorem smoothInteger_interval (φ : ℝ → ℝ) (G center : ℝ) (F : ℕ → ℂ) :
       (∑ p ∈ Finset.Ioc ⌊Real.exp (G - 1)⌋₊ ⌊Real.exp (G + 1)⌋₊,
         (φ (Real.log p - G) : ℂ) * F p) =
       (Real.exp center : ℂ) * complexIntegerInterval 1 0 (G - 1) (G + 1) center
         (fun x => (φ (x - G) : ℂ) * F ⌊Real.exp x⌋₊) := by
   …

   Mentions: OAI.Ostmann.complexIntegerInterval

2. theorem OAI.Ostmann.smoothGiant_integer_interval line 36

   Source documentation

   The remaining giant is averaged with its original normalized harmonic prior; no endpoint prime is deleted.

   theorem smoothGiant_integer_interval (φ : ℝ → ℝ) (G H center : ℝ)
       (hout : ∀ x, 1 ≤ |x| → φ x = 0) (F : ℕ → ℕ → ℂ) :
       (∑ q : smoothGiantPrimeRange H,
         (smoothGiantPrior (smoothGiantPrimeRange H) φ H q : ℂ) *
           ∑ p ∈ Finset.Ioc ⌊Real.exp (G - 1)⌋₊ ⌊Real.exp (G + 1)⌋₊,
             (φ (Real.log p - G) : ℂ) * F p q) =
       (Real.exp (smoothGiantLogNormalizer (smoothGiantPrimeRange H) φ H + center) : ℂ) *
         complexPrimeInterval 1 0 (H - 1) (H + 1) (fun y =>
           complexIntegerInterval 1 0 (G - 1) (G + 1) center (fun x =>
             (φ (x - G) : ℂ) * (φ (y - H) : ℂ) * F ⌊Real.exp x⌋₊ ⌊Real.exp y⌋₊)) := by
   …

   Mentions: OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.smoothGiantPrior, OAI.Ostmann.smoothGiantLogNormalizer, OAI.Ostmann.complexPrimeInterval, OAI.Ostmann.complexIntegerInterval

3. theorem OAI.Ostmann.smoothGiant_mixed_external_interval line 66

   Source documentation

   Finite Fubini retains the original regular law and counting measure on frequencies, as well as the exact giant and integer normalizations.

   theorem smoothGiant_mixed_external_interval {A B : Type*} [Fintype A] [Fintype B]
       (ν : B → A → ℝ) (N : ℕ) (φ : ℝ → ℝ) (G H center : ℝ)
       (hout : ∀ x, 1 ≤ |x| → φ x = 0)
       (F : ℤ → (B → A) → ℕ → ℕ → ℂ) :
       (∑ s : transferFrequencyRange N, ∑ x : B → A, ((∏ i, ν i (x i) : ℝ) : ℂ) *
         ∑ q : smoothGiantPrimeRange H,
           (smoothGiantPrior (smoothGiantPrimeRange H) φ H q : ℂ) *
             ∑ p ∈ Finset.Ioc ⌊Real.exp (G - 1)⌋₊ ⌊Real.exp (G + 1)⌋₊,
               (φ (Real.log p - G) : ℂ) * F s.val x p q) =
       (Real.exp (smoothGiantLogNormalizer (smoothGiantPrimeRange H) φ H + center) : ℂ) *
         mixedExternalAverage ν N (G - 1) (G + 1) (H - 1) (H + 1) center
           (fun s x z y => (φ (z - G) : ℂ) * (φ (y - H) : ℂ) *
   …

   Mentions: OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.smoothGiantPrior, OAI.Ostmann.smoothGiantLogNormalizer, OAI.Ostmann.mixedExternalAverage