OAI/NumberTheory/Ostmann/Arithmetic/MovingDiagonalIntegralScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingDiagonalOuterWeight_denormalize line 12
2. theorem OAI.Ostmann.movingPattern_diagonal_integral_norm line 27

   Source documentation

   The normalized multiplier costs only its fixed outer majorant after both integrals and the original signed pattern average.

   theorem movingPattern_diagonal_integral_norm {A B C J : Type*}
       [Fintype A] [Fintype B] [Fintype C] [Fintype J] {N n : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (prime : A → ℕ) (μ : ℕ → A → ℝ) (ν : B → A → ℝ)
       (pattern : Bool × MovingSampleIndex n → C)
       (reg : J → Fin (N + 1)) (active : J → Bool)
       (φ : ℝ → ℝ) (Jleft Jright Bφ Dφ : ℝ) (diagonal : Bool)
       (raw : ℝ → ℝ → (Fin (N + 1) → A) → ℂ)
       (haar : (Fin (N + 1) → A) → ℂ) (u v a b center bound : ℝ)
       (hbound : ‖∑ x, movingOriginalPatternWeight e μ ν prime n pattern
         (fun x => ∫ z in Set.Ioc u v, ∫ y in Set.Ioc a b,
           (movingDiagonalOuterWeight prime reg active φ Jleft Jright Bφ Dφ diagonal z y x *
             raw z y x) * (Real.exp (z - center) : ℂ) / (y : ℂ)) x * haar x‖ ≤ bound) :
   …

   Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingOriginalPatternWeight, OAI.Ostmann.movingDiagonalOuterWeight