RecursiveTransferWeight.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The recursive weight with its actual reconstructed integer pivots

def OAI.Ostmann.historyPivot line 13
theorem OAI.Ostmann.ValidTransferNode.historyPivot_eq line 17

def OAI.Ostmann.recursiveTransferWeight line 24

Source documentation

The node indicator contains precisely the arithmetic support used for history rigidity. Other original range/bin cutoffs are carried by cutoff.

noncomputable def recursiveTransferWeight {State : Type*} (sys : TransferHistorySystem State)
    (leaf : State → ℤ → ℂ) (cutoff : State → ℤ → ℤ → ℤ → ℝ) :
    (n : ℕ) → State → FrequencyTree ℤ n → ℂ
  | 0, σ, v => leaf σ v
  | n + 1, σ, t =>
      let v := frequencyRoot n t.2.1
…

Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.frequencyRoot

theorem OAI.Ostmann.recursiveTransferWeight_node line 40

Source documentation

No witness choices enter the recursive weight: the integer equation forces the pivot at every valid node.

theorem recursiveTransferWeight_node {State : Type*} (sys : TransferHistorySystem State)
    (leaf : State → ℤ → ℂ) (cutoff : State → ℤ → ℤ → ℤ → ℝ)
    (n : ℕ) (σ : State) (t : FrequencyTree ℤ (n + 1)) (P : ℕ)
    (hP : ValidTransferNode sys σ t.1 (frequencyRoot n t.2.1) (frequencyRoot n t.2.2) P) :
    recursiveTransferWeight sys leaf cutoff (n + 1) σ t =
      (cutoff σ t.1 (frequencyRoot n t.2.1) (frequencyRoot n t.2.2) : ℂ) *
        recursiveTransferWeight sys leaf cutoff n (sys.leftState σ P) t.2.1 *
        star (recursiveTransferWeight sys leaf cutoff n (sys.rightState σ P) t.2.2) := by
…

Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ValidTransferNode, OAI.Ostmann.frequencyRoot, OAI.Ostmann.recursiveTransferWeight

theorem OAI.Ostmann.recursiveTransferWeight_nonzero_valid line 50

theorem OAI.Ostmann.recursiveTransferWeight_square_le line 72

Source documentation

Each squaring doubles the number of bottom weights and never adds an absolute-value loss for a cutoff or an invalid arithmetic node.

theorem recursiveTransferWeight_square_le {State : Type*} (sys : TransferHistorySystem State)
    (leaf : State → ℤ → ℂ) (cutoff : State → ℤ → ℤ → ℤ → ℝ)
    (B : ℝ) (hB : 0 ≤ B) (hleaf : ∀ σ v, ‖leaf σ v‖ ^ 2 ≤ B)
    (hcut : ∀ σ s v w, |cutoff σ s v w| ≤ 1)
    (n : ℕ) (σ : State) (t : FrequencyTree ℤ n) :
    ‖recursiveTransferWeight sys leaf cutoff n σ t‖ ^ 2 ≤ B ^ (2 ^ n) := by
…

Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight

theorem OAI.Ostmann.recursiveTransferWeight_square_exp_le line 97

Source documentation

The manuscript's level-zero modulus window gives the full history square bound, with exactly 2^n copies of its exponent.

theorem recursiveTransferWeight_square_exp_le {State : Type*} (sys : TransferHistorySystem State)
    (leaf : State → ℤ → ℂ) (cutoff : State → ℤ → ℤ → ℤ → ℝ)
    (Δ K : ℝ) (hleaf : ∀ σ v, ‖leaf σ v‖ ^ 2 ≤ Real.exp (-Δ + K))
    (hcut : ∀ σ s v w, |cutoff σ s v w| ≤ 1)
    (n : ℕ) (σ : State) (t : FrequencyTree ℤ n) :
    ‖recursiveTransferWeight sys leaf cutoff n σ t‖ ^ 2 ≤
      Real.exp (-(2 ^ n : ℕ) * Δ + (2 ^ n : ℕ) * K) := by
…

Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight

theorem OAI.Ostmann.archimedeanLeafFactor_square_exp_le line 111

Source documentation

The leaf estimate is derived from the product window on every nonzero cutoff, including its boundary. It is not a new norm hypothesis.

theorem archimedeanLeafFactor_square_exp_le (X M s c Δ C K : ℝ)
    (ψhat : ℝ → ℂ) (hc : |c| ≤ 1)
    (hψ : ∀ u, ‖ψhat u‖ ≤ Real.exp K)
    (hwindow : c ≠ 0 → 0 < M ∧ X * Real.exp (Δ - C) ≤ M) :
    ‖archimedeanLeafFactor X M s c ψhat‖ ^ 2 ≤ Real.exp (-Δ + (C + 2 * K)) := by
…

Mentions: OAI.Ostmann.archimedeanLeafFactor

theorem OAI.Ostmann.recursive_archimedean_square_exp_le line 135

Source documentation

The recursively substituted coefficient inherits its square bound from the actual initial product ranges and Fourier bound.

theorem recursive_archimedean_square_exp_le {State : Type*}
    (sys : TransferHistorySystem State) (M : State → ℕ) (c : State → ℤ → ℝ)
    (cutoff : State → ℤ → ℤ → ℤ → ℝ) (X Δ C K : ℝ) (ψhat : ℝ → ℂ)
    (hc : ∀ σ v, |c σ v| ≤ 1) (hψ : ∀ u, ‖ψhat u‖ ≤ Real.exp K)
    (hwindow : ∀ σ v, c σ v ≠ 0 → 0 < M σ ∧ X * Real.exp (Δ - C) ≤ M σ)
    (hcut : ∀ σ s v w, |cutoff σ s v w| ≤ 1)
    (n : ℕ) (σ : State) (t : FrequencyTree ℤ n) :
    ‖recursiveTransferWeight sys
      (fun σ v => archimedeanLeafFactor X (M σ) v (c σ v) ψhat) cutoff n σ t‖ ^ 2 ≤
      Real.exp (-(2 ^ n : ℕ) * Δ + (2 ^ n : ℕ) * (C + 2 * K)) := by
…

Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.archimedeanLeafFactor