OAI/NumberTheory/Ostmann/Arithmetic/MovingOriginalSampleExpansion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingOriginalLeaf line 10
2. def OAI.Ostmann.movingOriginalNode line 17
3. theorem OAI.Ostmann.movingOriginalNode_local line 22
4. theorem OAI.Ostmann.movingOriginalNode_compensated line 30
5. def OAI.Ostmann.movingOriginalSampleAverage line 41

   Source documentation

   The sampled Fourier coefficient, with all original support and all original internal probabilities.

   noncomputable def movingOriginalSampleAverage {σ I : Type*} [Fintype σ]
       (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
       (μ : ℕ → σ → ℝ) (childBound pivotBound : ℕ → ℕ)
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n) (XL XR : ℕ) : ℂ :=
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple

6. theorem OAI.Ostmann.movingOriginalSampleAverage_eq line 55

   Source documentation

   The Fourier/window/spectator coefficient is exactly the local sampled recursion already expanded above.

   theorem movingOriginalSampleAverage_eq {σ I : Type*} [Fintype σ]
       (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
       (μ : ℕ → σ → ℝ) (childBound pivotBound : ℕ → ℕ)
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n) (XL XR : ℕ) :
       movingOriginalSampleAverage q value outside μ childBound pivotBound F g Dq S ψ X lo hi φ G
         n t small bulk XL XR =
       movingSupportedSampledWeight value outside μ childBound pivotBound
         (movingOriginalLeaf value q F g Dq S ψ X lo hi)
         (movingOriginalNode value childBound pivotBound φ G) n t small bulk XL XR := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingOriginalSampleAverage, OAI.Ostmann.movingSupportedSampledWeight, OAI.Ostmann.movingOriginalLeaf, OAI.Ostmann.movingOriginalNode

7. theorem OAI.Ostmann.movingSupportedSampleTerm_original line 74

   Source documentation

   After extracting compensation, the retained term is the original giant coefficient with unit data at internal nodes.

   theorem movingSupportedSampleTerm_original {σ I : Type*}
       (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
       (childBound pivotBound : ℕ → ℕ)
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n) (XL XR : ℕ)
       (a : MovingSampleSlots σ n) :
       movingSupportedSampleTerm value outside childBound pivotBound
         (movingOriginalLeaf value q F g Dq S ψ X lo hi)
         (movingOriginalNode value childBound pivotBound φ G) n t small bulk XL XR a =
       movingSupportedWeight value outside (buildMovingSlotData n t small bulk a) XL XR
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingSupportedSampleTerm, OAI.Ostmann.movingOriginalLeaf, OAI.Ostmann.movingOriginalNode, OAI.Ostmann.movingSupportedWeight, OAI.Ostmann.buildMovingSlotData