MovingSegmentWeights.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Endpoint weight motion from the relative parent and boundary losses. The full-root loss is used only at the snapshot.

theorem OAI.LipschitzHilbert.segmentLog_re_le_of_log_motion line 14

theorem OAI.LipschitzHilbert.moving_segmentWeight_variation line 32

Source documentation

The moving endpoint-plus-variation estimate on any later segment. All error factors multiply the original loss budget, never the depth.

theorem moving_segmentWeight_variation (n n' R R' : ℕ → ℝ) (phase : ℕ → ℂ)
    (start N K : ℕ) (hstart : start ≤ N) (a Z δ ε lower : ℝ)
    (ha : 0 ≤ a) (hZ : 0 ≤ Z) (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (hlower : 0 < lower)
    (hn : ∀ j ≤ N, lower ≤ n j) (hn' : ∀ j ≤ N, 0 < n' j)
    (hmono : AntitoneOn n (Set.Iic N))
    (hR0 : ∀ j < N, 0 ≤ R j) (hR0' : ∀ j < N, 0 ≤ R' j)
    (hR : ∀ j < N, R j ≤ Real.log (n (j+1-K)/n (j+1)))
    (hz0 : ∀ j < N, 0 ≤ (phase j).re) (hz : ∀ j < N, ‖phase j‖ ≤ Z)
    (hmass : ∀ j, start ≤ j → j ≤ N → |Real.log (n' j)-Real.log (n j)| ≤ δ)
    (hPmove : ∀ j ∈ Finset.Ico start N,
      |Real.log (n' j/n' (j+1))-Real.log (n j/n (j+1))| ≤ ε*Real.log (n j/n (j+1)))
    (hRmove : ∀ j ∈ Finset.Ico start N, |R' j-R j| ≤ ε*R j) :
…