OAI/NumberTheory/Ostmann/Arithmetic/MovingCoefficientSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingFullSupport_local line 11
2. theorem OAI.Ostmann.movingSupportedSampledWeight_nonzero_support line 21

   Source documentation

   A nonzero finite average contains a supported original sample. No positivity, normalization, or conditioning of the prime prior is needed.

   theorem movingSupportedSampledWeight_nonzero_support {σ : Type*} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
       (XL XR : ℕ)
       (h : movingSupportedSampledWeight value outside μ childBound pivotBound F E
         n t small bulk XL XR ≠ 0) :
       ∃ a : MovingSampleSlots σ n,
         movingFullSupport value outside (buildMovingSlotData n t small bulk a) XL XR := by
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingSupportedSampledWeight, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingFullSupport, OAI.Ostmann.buildMovingSlotData

3. theorem OAI.Ostmann.movingFrequencyCoefficient_nonzero_support line 45

   Source documentation

   The root sum still has the actual current pairwise support and both root-frequency units. These are the only support facts needed to attach the original coefficient to the full Fourier transfer.

   theorem movingFrequencyCoefficient_nonzero_support {σ : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ) (s : ℤ)
       (small bulk : TreeLeafTuple (List σ) n) (XL XR : ℕ)
       (h : movingFrequencyCoefficient value outside μ childBound pivotBound V F φ G
         n s small bulk XL XR ≠ 0) :
       (XL :: XR :: ((flattenMovingSlots n small ++ flattenMovingSlots n bulk).map value ++ outside)).Pairwise Nat.Coprime ∧
         IsCoprime (XL : ℤ) s ∧ IsCoprime (XR : ℤ) s := by
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingFrequencyCoefficient, OAI.Ostmann.flattenMovingSlots