MovingSegmentLogs.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The initial value and loss budget for the actual moving segment logarithms. The total cost is paid by the full-root loss, including when another shift's block begins before the segment.

def OAI.LipschitzHilbert.segmentCost line 15

theorem OAI.LipschitzHilbert.segmentLog_initial_motion line 20

Source documentation

At the starting endpoint the transition product is empty, so only the one initial mass logarithm moves.

theorem segmentLog_initial_motion (n n' R R' : ℕ → ℝ) (phase : ℕ → ℂ)
    (a delta : ℝ) (start : ℕ) (ha : 0 ≤ a)
    (hlog : |Real.log (n' start)-Real.log (n start)| ≤ delta) :
    ‖segmentLog n' R' phase a start start-segmentLog n R phase a start start‖ ≤ a*delta := by
…

Mentions: OAI.LipschitzHilbert.segmentLog

theorem OAI.LipschitzHilbert.segmentCost_nonnegative line 32
theorem OAI.LipschitzHilbert.segmentLog_increment_le_cost line 37

theorem OAI.LipschitzHilbert.segmentCost_sum_le_full_root line 49

Source documentation

Summing the nonnegative costs on any later segment uses the full-root logarithm rather than a factor counting hierarchy levels.

theorem segmentCost_sum_le_full_root (n R : ℕ → ℝ) (start N K : ℕ)
    (a Z : ℝ) (ha : 0 ≤ a) (hZ : 0 ≤ Z)
    (hn : ∀ j ≤ N, 0 < n j) (hmono : AntitoneOn n (Set.Iic N))
    (hR0 : ∀ j < N, 0 ≤ R j)
    (hR : ∀ j < N, R j ≤ Real.log (n (j+1-K)/n (j+1))) :
    (∑ j ∈ Finset.Ico start N, segmentCost n R a Z j) ≤
      (a+Z*K)*Real.log (n 0/n N) := by
…

Mentions: OAI.LipschitzHilbert.segmentCost

theorem OAI.LipschitzHilbert.AngularGrid.source_segment_initial_motion line 77

Source documentation

The actual starting cell supplies the initial moving-log estimate. The boundary-loss sequences do not enter at this endpoint.

theorem source_segment_initial_motion {ι : Type*} (g : AngularGrid) (tops : Finset ι)
    (T : ι → SlopeBox) (w B K D : ℝ) (hw : 0 < w) (hB : 1 ≤ B)
    (hK : 0 < K) (hD : 0 ≤ D) (hwidth : ∀ t ∈ tops, B^2*w ≤ (T t).width)
    (h start : ℕ) (hh : h ≤ start) (gap : ℝ) (hgap0 : 0 ≤ gap) (hgap : gap ≤ g.width h)
    (top : ι) (htop : top ∈ tops)
    (he : g.eligible (g.rootWidth/B^2) (w/(T top).length) start)
    (sR : ℝ) (hs : g.index h (T top).slope = g.index h sR)
    (child : ℝ) (hchild : 0 < child) (hblock : g.width h ≤ B*child)
    (a : ℝ) (ha : |a| ≤ w/(child*Real.sqrt (g.branching:ℝ))) (z : ℝ × ℝ)
    (R0 R1 : ℕ → ℝ) (phase : ℕ → ℂ) (exponent : ℝ) (hexponent : 0 ≤ exponent) :
    let n := fun x j => g.mass tops (fun t => (T t).slope) (fun t => w/(T t).length)
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.AngularGrid.width

theorem OAI.LipschitzHilbert.AngularGrid.source_segment_log_budget line 105

Source documentation

Actual eligible-top masses supply every initial-increment and budget hypothesis for moving exponential segment weights.

theorem source_segment_log_budget {ι X : Type*} (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (hw : ∀ t x, 0 < weight t x)
    {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
    (start N : ℕ) (top : ι) (htop : top ∈ tops)
    (he : g.eligible cutoff (precision top) N) (x : X)
    (a Z : ℝ) (ha : 0 ≤ a) (hZ : 0 ≤ Z) (hphase : ∀ j < N, ‖phase j‖ ≤ Z) :
    let n := fun j => g.mass tops slope precision cutoff weight j (g.index j (slope top)) x
…

Mentions: OAI.LipschitzHilbert.AngularGrid