OAI/NumberTheory/Ostmann/Arithmetic/MovingBulkOriginalCoefficient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingBulkLeafProduct_bounds line 10
2. theorem OAI.Ostmann.movingOriginalLeaf_bulk_log line 21
3. theorem OAI.Ostmann.movingFrequencyCoefficient_original_bulk_log line 37

   Source documentation

   All sharp windows, Fourier factors, spectator factors and support tests remain in the coefficient after the real bulk weight has been extracted.

   theorem movingFrequencyCoefficient_original_bulk_log {σ I : Type} [Fintype σ]
       (value tier : σ → ℕ) (k : ℕ) (outside : List ℕ) (cb cd : ℝ)
       (μ : ℕ → σ → ℝ) (hμ : ∀ j a, μ j a ≠ 0 → tier a = j)
       (q : I → ℕ) [∀ i, Fact (q i).Prime]
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ)
       (childBound pivotBound V : ℕ → ℕ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n : ℕ) (s : ℤ) (small bulk : TreeLeafTuple (List σ) n)
       (hn : n ≤ k) (hsmall : ∀ i ∈ flattenMovingSlots n small, tier i ≠ k)
       (hbulk : ∀ i ∈ flattenMovingSlots n bulk, tier i = k) (XL XR : ℕ) :
       movingFrequencyCoefficient value outside μ childBound pivotBound V
   …

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

4. theorem OAI.Ostmann.movingFrequencyCoefficient_original_bulk_log_norm_le line 68

   Source documentation

   Pointwise domination applies before any external bulk symmetrization. It supplies the original same-assignment energy bound with the cutoffs retained.

   theorem movingFrequencyCoefficient_original_bulk_log_norm_le {σ I : Type} [Fintype σ]
       (value tier : σ → ℕ) (k : ℕ) (outside : List ℕ) (cb cd : ℝ)
       (μ : ℕ → σ → ℝ) (hμ : ∀ j a, μ j a ≠ 0 → tier a = j)
       (q : I → ℕ) [∀ i, Fact (q i).Prime]
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ)
       (childBound pivotBound V : ℕ → ℕ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n : ℕ) (s : ℤ) (small bulk : TreeLeafTuple (List σ) n)
       (hn : n ≤ k) (hsmall : ∀ i ∈ flattenMovingSlots n small, tier i ≠ k)
       (hbulk : ∀ i ∈ flattenMovingSlots n bulk, tier i = k) (XL XR : ℕ) :
       ‖movingFrequencyCoefficient value outside μ childBound pivotBound V
   …

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