MovingGiantTree.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The moving-giant arithmetic in Section 8.1

The integer constants record actual products of regular small entries. At a reversal, the sampled compensation product u is inserted into both children: their constants are u * CL and u * CR. The pivot is reconstructed over the integers first, and only its giant factor is passed to either child.

inductive OAI.Ostmann.MovingGiantTree line 18
def OAI.Ostmann.MovingGiantTree.frequency line 24
def OAI.Ostmann.movingGiantPivot line 29

theorem OAI.Ostmann.movingGiantPivot_of_node line 34

Source documentation

This is the exact division in (8.3), applied to a valid original node.

theorem movingGiantPivot_of_node {State : Type*}
    {sys : TransferHistorySystem State} {σ : State} {s v w : ℤ} {P : ℕ}
    (h : ValidTransferNode sys σ s v w P) (CL CR u p XL XR ML MR : ℕ)
    (hu : 0 < u) (hP : P = u * p)
    (hL : sys.leftProduct σ = XL * CL * ML)
    (hR : sys.rightProduct σ = XR * CR * MR) :
    movingGiantPivot s v w CL CR u XL XR ML MR = p := by
…

Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.ValidTransferNode, OAI.Ostmann.movingGiantPivot

def OAI.Ostmann.MovingGiantTree.Integral line 45
def OAI.Ostmann.MovingGiantTree.UnitsAt line 57
def OAI.Ostmann.TreeNaturalLift line 63
theorem OAI.Ostmann.TreeNaturalLift.product line 68

def OAI.Ostmann.movingGiantAmplitude line 80

Source documentation

Ordinary integral evaluation, including the inserted-giant zero convention. All additional smooth and range factors can multiply this spectator factor.

noncomputable def movingGiantAmplitude {q : ℕ} [Fact q.Prime]
    (g : ZMod q → ℂ) (D : (ZMod q)ˣ) :
    {n C : ℕ} → MovingGiantTree n C → ℕ → ℕ → TreeLeafTuple ℕ n → ℂ
  | _, _, .leaf s C, XL, XR, x =>
      g ((s : ZMod q) / ((D : ZMod q) * ((XL * XR * C * treeLeafProduct 0 x : ℕ) : ZMod q)))
  | n + 1, _, .node s CL CR u left right, XL, XR, x =>
      let p := movingGiantPivot s left.frequency right.frequency CL CR u XL XR
…

Mentions: OAI.Ostmann.MovingGiantTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.movingGiantPivot

theorem OAI.Ostmann.MovingGiantTree.exists_residue_diagram line 95

Source documentation

Every integral moving-giant history has a rational diagram whose constants and frequencies depend only on the fixed small data and frequency history. They do not depend on the giant values or on the bulk leaf values.

theorem MovingGiantTree.exists_residue_diagram {q : ℕ} [Fact q.Prime]
    {n C : ℕ} (T : MovingGiantTree n C) (hT : T.UnitsAt q) :
    ∃ (U : (ZMod q)ˣ) (R : RationalTreeData (ZMod q)ˣ n U),
      (C : ZMod q) = U ∧ (T.frequency : ZMod q) = R.frequency ∧
      ∀ (g : ZMod q → ℂ) (D : (ZMod q)ˣ) (XL XR : ℕ)
        (A B : (ZMod q)ˣ) (x : TreeLeafTuple ℕ n) (y : TreeLeafTuple (ZMod q)ˣ n),
        (XL : ZMod q) = A → (XR : ZMod q) = B → TreeNaturalLift n x y →
        T.Integral XL XR x → ∀ b : Bool,
        (if b then conj (movingGiantAmplitude g D T XL XR x)
          else movingGiantAmplitude g D T XL XR x) =
          rationalTreeAmplitude g D R A B (transferConjugations n b) y := by
…

Mentions: OAI.Ostmann.MovingGiantTree, OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeNaturalLift, OAI.Ostmann.movingGiantAmplitude, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.transferConjugations