OAI/NumberTheory/Ostmann/Arithmetic/MovingSupportedWeight.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingFullSupport line 11
2. def OAI.Ostmann.movingSupportedWeight line 17

   Source documentation

   Multiplying by this mask retains all current-state coprimality and all subtree-frequency unit tests, including the fixed outside list.

   noncomputable def movingSupportedWeight {σ : Type*} (value : σ → ℕ) (outside : List ℕ)
       {n : ℕ} (T : MovingSlotData σ n) (XL XR : ℕ) (z : ℂ) : ℂ :=
   …

   Mentions: OAI.Ostmann.MovingSlotData

3. def OAI.Ostmann.movingResidueSupportedWeight line 21
4. theorem OAI.Ostmann.movingResidueSupportedWeight_norm line 25
5. theorem OAI.Ostmann.movingSupportedWeight_residue line 31
6. theorem OAI.Ostmann.movingOriginalGiantWeight_integral line 52
7. theorem OAI.Ostmann.movingOriginalGiantWeight_full_factor line 68

   Source documentation

   Exact factorization of the fully supported coefficient, with the single nonperiodic top-pair coprimality indicator still visible.

   theorem movingOriginalGiantWeight_full_factor {σ I : Type*} (q : I → ℕ)
       [∀ i, Fact (q i).Prime] (tier : σ → ℕ) (value : σ → ℕ)
       (hprime : ∀ i, (value i).Prime) (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
       (outside : List ℕ) (childBound pivotBound : ℕ → ℕ)
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       (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)
   …

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