MovingDerivedProductStep.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Transfer with the product cap proved from the original terminal window

theorem OAI.Ostmann.movingTemplatePrimeAmplitude_step_of_cells line 16

Source documentation

Both the product cap and the next amplitude are derived from the original coefficient. The remaining hypotheses are the numerical range and separation conditions of the concrete prime-cell construction.

theorem movingTemplatePrimeAmplitude_step_of_cells {σ J : Type} [Fintype σ]
    (value : σ → ℕ) (hvalue : ∀ a, (value a).Prime)
    (outside : List ℕ) (μ : ℕ → σ → ℝ)
    (childBound pivotBound V : ℕ → ℕ) (hV : Monotone V)
    (q : J → ℕ) [∀ i, Fact (q i).Prime]
    (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
    (hF : ∀ {n} (T : MovingSlotData σ n), F T 0 = 0)
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset J)
    (ψ : SchwartzMap ℝ ℂ) (X lo hi W : ℝ) (hX : 0 < X)
    (hwindow : X * hi ≤ Real.exp W)
    (φ : ℝ → ℝ) (G c : ℕ → ℝ) (hout : ∀ t, 1 ≤ |t| → φ t = 0)
    (hμlower : ∀ j x, μ j x ≠ 0 → Real.exp (c j - 1) ≤ (value x : ℝ))
…

Mentions: OAI.Ostmann.MovingSlotData