MovingGiantArchimedean.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The actual terminal moduli as quadratic functions of a top giant

Small prime values are fixed here. Every reconstructed giant is linear in the initial pair, and each terminal modulus is a product of two such linear forms. The identification uses the integer support equations of the original sampler.

def OAI.Ostmann.MovingSlotReversal.realPivot line 18
theorem OAI.Ostmann.MovingSlotReversal.realPivot_eq line 24
def OAI.Ostmann.MovingSlotReversal.pivotPolynomial line 36
theorem OAI.Ostmann.MovingSlotReversal.pivotPolynomial_eval line 45
theorem OAI.Ostmann.MovingSlotReversal.pivotPolynomial_degree line 52

def OAI.Ostmann.MovingSlotData.leafModuli line 65

Source documentation

The terminal integer moduli, with the same pivot divisions and child order as the full recursive coefficient.

def MovingSlotData.leafModuli {σ : Type*} (value : σ → ℕ) :
    {n : ℕ} → MovingSlotData σ n → ℕ → ℕ → TreeLeafIndex n → ℕ
  | _, .leaf _ regular, XL, XR, _ => XL * XR * MovingSlotReversal.naturalProduct value regular
  | _, .node s CL CR u left right, XL, XR, i =>
      let p := (MovingSlotData.step s CL CR u left right false).naturalPivot value XL XR
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.MovingSlotData.step

def OAI.Ostmann.MovingSlotData.leafPolynomials line 76

Source documentation

Polynomial extension in one free top coordinate. Its coefficients may contain reciprocals of the fixed frequency and compensation products.

noncomputable def MovingSlotData.leafPolynomials {σ : Type*} (value : σ → ℕ) :
    {n : ℕ} → MovingSlotData σ n → Polynomial ℝ → Polynomial ℝ →
      TreeLeafIndex n → Polynomial ℝ
  | _, .leaf _ regular, XL, XR, _ =>
      XL * XR * Polynomial.C (MovingSlotReversal.naturalProduct value regular : ℝ)
  | _, .node s CL CR u left right, XL, XR, i =>
      let p := (MovingSlotData.step s CL CR u left right false).pivotPolynomial value XL XR
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.MovingSlotData.step

theorem OAI.Ostmann.MovingSlotData.leafPolynomials_degree line 87
theorem OAI.Ostmann.MovingSlotReversal.naturalProduct_ne_zero line 103

theorem OAI.Ostmann.MovingSlotData.leafPolynomials_eval line 113

Source documentation

Exact agreement on integer support; no approximation or extra real-variable realization condition is assumed.

theorem MovingSlotData.leafPolynomials_eval {σ : Type*} (value : σ → ℕ)
    (hvalue : ∀ i, value i ≠ 0) {n : ℕ} (T : MovingSlotData σ n)
    (hfreq : T.Frequencies (· ≠ 0)) (XL XR : ℕ) (hI : T.Integral value XL XR)
    (L R : Polynomial ℝ) (z : ℝ) (hL : L.eval z = (XL : ℝ)) (hR : R.eval z = (XR : ℝ))
    (i : TreeLeafIndex n) :
    (T.leafPolynomials value L R i).eval z = (T.leafModuli value XL XR i : ℝ) := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafIndex

theorem OAI.Ostmann.MovingSlotData.leftGiant_quadratic line 134

Source documentation

In particular each leaf is quadratic in either initial giant.

theorem MovingSlotData.leftGiant_quadratic {σ : Type*} (value : σ → ℕ)
    {n : ℕ} (T : MovingSlotData σ n) (XR : ℝ) (i : TreeLeafIndex n) :
    (T.leafPolynomials value Polynomial.X (Polynomial.C XR) i).natDegree ≤ 2 := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafIndex