FullAtomWeightSupport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Support and square-energy bounds for the actual full atom weight

theorem OAI.Ostmann.fullAtomTransferWeight_support line 11
theorem OAI.Ostmann.fullAtomTransferWeight_top_support line 24

theorem OAI.Ostmann.fullAtomTransferWeight_square_exp_le line 37

Source documentation

All added guards are exact zero-one cutoffs and cannot increase energy.

theorem fullAtomTransferWeight_square_exp_le {I : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
    (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
    (leaf : ScheduleAtomState role → ℤ → ℂ) (Δ K : ℝ)
    (hleaf : ∀ σ v, ‖leaf σ v‖ ^ 2 ≤ Real.exp (-Δ + K))
    (n : ℕ) (x : CopyScheduleAtoms role n → ℕ) (t : FrequencyTree ℤ n) :
    ‖fullAtomTransferWeight role childBound pivotBound ranges leaf n x t‖ ^ 2 ≤
      Real.exp (-(2 ^ n : ℕ) * Δ + (2 ^ n : ℕ) * K) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.FrequencyTree, OAI.Ostmann.fullAtomTransferWeight