MovingWeightBudget.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite endpoint transport from the actual logarithmic loss budget. Small relative errors are summed against losses, without charging a fixed error for every hierarchy level.

theorem OAI.LipschitzHilbert.exponential_weight_motion_from_increments line 14

theorem OAI.LipschitzHilbert.exponential_weight_motion_on_interval line 56

Source documentation

The same transport bound on any interval of later endpoints.

theorem exponential_weight_motion_on_interval (L M : ℕ → ℂ) (cost : ℕ → ℝ)
    (start N : ℕ) (hstart : start ≤ N) (C D ε V : ℝ)
    (hD : 0 ≤ D) (hε : 0 ≤ ε) (hV : 0 ≤ V)
    (hL : ∀ j, start ≤ j → j ≤ N → (L j).re ≤ C)
    (hM : ∀ j, start ≤ j → j ≤ N → (M j).re ≤ C)
    (hzero : ‖M start-L start‖ ≤ D)
    (hcost : ∀ j ∈ Finset.Ico start N, 0 ≤ cost j)
    (hincr : ∀ j ∈ Finset.Ico start N, ‖L (j+1)-L j‖ ≤ cost j)
    (hmove : ∀ j ∈ Finset.Ico start N,
      ‖(M (j+1)-M j)-(L (j+1)-L j)‖ ≤ ε*cost j)
    (hbudget : (∑ j ∈ Finset.Ico start N, cost j) ≤ V) :
    ‖Complex.exp (M N)-Complex.exp (L N)‖ +
…

theorem OAI.LipschitzHilbert.segmentLog_increment_motion line 89

Source documentation

A moving endpoint increment is controlled by relative errors in the parent loss and boundary loss, with exactly the original weighted cost.

theorem segmentLog_increment_motion (n n' R R' : ℕ → ℝ) (phase : ℕ → ℂ)
    (a ε Z : ℝ) (start j : ℕ) (hs : start ≤ j)
    (ha : 0 ≤ a) (hZ : 0 ≤ Z)
    (hn : 0 < n j) (hn1 : 0 < n (j+1))
    (hn' : 0 < n' j) (hn1' : 0 < n' (j+1))
    (hP : |Real.log (n' j/n' (j+1))-Real.log (n j/n (j+1))| ≤
      ε*Real.log (n j/n (j+1)))
    (hR : |R' j-R j| ≤ ε*R j) (hz : ‖phase j‖ ≤ Z) :
    ‖(segmentLog n' R' phase a start (j+1)-segmentLog n' R' phase a start j)-
      (segmentLog n R phase a start (j+1)-segmentLog n R phase a start j)‖ ≤
      ε*(a*Real.log (n j/n (j+1))+Z*R j) := by
…

Mentions: OAI.LipschitzHilbert.segmentLog