OAI/NumberTheory/Ostmann/Arithmetic/MovingInitialCoefficient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingFrequencyCoefficient_levelZero_sample line 10
2. theorem OAI.Ostmann.movingFrequencyCoefficient_levelZero line 23
3. theorem OAI.Ostmann.movingFrequencyCoefficient_levelZero_support line 39
4. theorem OAI.Ostmann.movingOriginalLeaf_window line 52
5. theorem OAI.Ostmann.movingFrequencyCoefficient_initial_window line 66
6. theorem OAI.Ostmann.movingFrequencyCoefficient_initial_retained_bound line 90

   Source documentation

   At the first step the original terminal window bounds the retained product after the extracted giant and compensation product are removed.

   theorem movingFrequencyCoefficient_initial_retained_bound {σ I : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (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 lower : ℝ) (hX : 0 < X)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (s : ℤ)
       (comp small bulk : List σ) (p XR H : ℕ)
       (hp : 0 < p) (hcomp : 0 < MovingSlotReversal.naturalProduct value comp)
       (hlower : lower ≤ (p * MovingSlotReversal.naturalProduct value comp : ℕ))
       (hcap : X * hi ≤ lower * H)
       (h : movingFrequencyCoefficient value outside μ childBound pivotBound V
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.movingFrequencyCoefficient