MovingFirstProductBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The first recursive product bound from the two original windows

theorem OAI.Ostmann.movingFrequencyCoefficient_one_product_bound line 11

Source documentation

Nonzero first-level coefficients retain both terminal windows. Removing the shared inner pivot from each gives a bound on the full current product.

theorem movingFrequencyCoefficient_one_product_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 : ℕ → ℝ)
    (hmin : ∀ a : Fin 4 → σ, movingCompensationPrior (μ 0) 0 a ≠ 0 →
      ∀ p : ℕ, 0 < p → φ (Real.log p - G 1) ≠ 0 →
        lower ≤ (p * MovingSlotReversal.naturalProduct value (List.ofFn a) : ℕ))
    (H : ℕ) (hcap : X * hi ≤ lower * H)
…

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

theorem OAI.Ostmann.movingFrequencyCoefficient_one_retained_bound line 43