OAI/NumberTheory/Ostmann/Arithmetic/MovingRealWindows.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.MovingSlotData.leafPolynomials_real line 12
2. theorem OAI.Ostmann.MovingSlotData.realLeafModuli_nat line 26
3. def OAI.Ostmann.movingRealWindowFlag line 34
4. theorem OAI.Ostmann.movingWindowedData_real_factor line 38
5. theorem OAI.Ostmann.moving_original_nonsmooth_residue_factor line 53

   Source documentation

   The original nonsmooth coefficient is exactly a fixed residue factor times a function of the two real giant coordinates. This includes zero terms.

   theorem moving_original_nonsmooth_residue_factor {σ I : Type*} (q : I → ℕ)
       [∀ i, Fact (q i).Prime] (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
       (childBound pivotBound : ℕ → ℕ)
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       (X lo hi : ℝ) (g : ∀ i, ZMod (q i) → ℂ) (D : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       {n : ℕ} (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) (XL XR a b M : ℕ)
       (hM : movingTopPeriod value hvalue childBound pivotBound T hf ∣ M)
       (hMq : ∀ i ∈ S, (q i : ℤ) * movingSpectatorDenominator value T ∣ (M : ℤ))
       (hL : (XL : ℤ) ≡ (a : ℤ) [ZMOD M]) (hR : (XR : ℤ) ≡ (b : ℤ) [ZMOD M]) :
       let nodes := T.formulaNodes value hvalue childBound pivotBound hf (.prime false) (.prime true)
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingTopPeriod, OAI.Ostmann.movingSpectatorDenominator