MovingFullSmoothZero.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Full smooth coefficients with only the actual spectator zero convention

theorem OAI.Ostmann.movingSlotWeight_spectator_product_of_zero line 13

Source documentation

Factor every spectator while retaining the full smooth and arithmetic coefficient. This identity includes zero-support terms.

theorem movingSlotWeight_spectator_product_of_zero {σ I : Type*}
    (q : I → ℕ) [∀ i, Fact (q i).Prime]
    (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ)
    (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (g : ∀ i, ZMod (q i) → ℂ) (hg : ∀ i, g i 0 = 0) (D : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
    (XL XR : ℕ) :
    recursiveTransferWeight (movingSlotSystem value childBound pivotBound)
        (fun x s => F x s * ∏ i ∈ S, spectatorHistoryLeaf (movingSlotModulus value) (g i) (D i) x s)
        (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t =
      recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.spectatorHistoryLeaf, OAI.Ostmann.movingSlotModulus, OAI.Ostmann.movingSlotCutoff

theorem OAI.Ostmann.moving_full_smooth_spectator_of_zero line 44

Source documentation

The complete moving coefficient splits into the original scalar support, its actual smooth polynomial weight, and all of its spectator trees. No nonzero-term hypothesis is needed.

theorem moving_full_smooth_spectator_of_zero {σ I : Type*}
    (q : I → ℕ) [∀ i, Fact (q i).Prime]
    (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ) (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (g : ∀ i, ZMod (q i) → ℂ) (hg : ∀ i, g i 0 = 0) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
    (φ : ℝ → ℝ) (G : ℕ → ℝ) (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
    (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
    (hout : ∀ x, 1 ≤ |x| → φ x = 0)
    {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
    (hfreq : T.Frequencies (· ≠ 0)) (XL XR : ℕ) (L R : Polynomial ℝ) (z : ℝ)
    (hL : L.eval z = (XL : ℝ)) (hR : R.eval z = (XR : ℝ)) :
…

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