MovingFirstExtendedWindows.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Both terminal windows survive extension of the outer giants to integers

theorem OAI.Ostmann.movingFrequencyCoefficient_one_extended_children line 12

Source documentation

A nonzero first node contains a nonzero pair of terminal coefficients, even when either outer giant has been extended to a positive integer. All original cross-branch support tests stay inside the selected summand.

theorem movingFrequencyCoefficient_one_extended_children {σ : Type} [Fintype σ]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
    (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
    (φ : ℝ → ℝ) (G : ℕ → ℝ) (s : ℤ)
    (small bulk : List σ × List σ) (XL XR : ℕ)
    (h : movingFrequencyCoefficient value outside μ childBound pivotBound V F φ G
      1 s small bulk XL XR ≠ 0) :
    ∃ (a : Fin 4 → σ) (v w : transferFrequencyRange (V 0)),
      let u := List.ofFn a
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.movingFrequencyCoefficient, OAI.Ostmann.transferFrequencyRange