AngularPathLossMotion.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The two logarithmic losses in an actual endpoint increment inherit relative motion from their concrete child, parent, and boundary top sets.

theorem OAI.LipschitzHilbert.AngularGrid.source_path_loss_motion line 16

Source documentation

Both P_i=log(n_i/n_(i+1)) and R_i=log(m_i/n_(i+1)) have relative motion at the source averaging scale. The second statement allows the boundary ancestor to begin before the current block.

theorem source_path_loss_motion {ι : Type*} (g : AngularGrid) (tops : Finset ι)
    (T : ι → SlopeBox) (w B Kw D : ℝ) (hw : 0 < w) (hB : 1 ≤ B)
    (hKw : 0 < Kw) (hD : 0 ≤ D) (hwidth : ∀ t ∈ tops, B^2*w ≤ (T t).width)
    {Kb : ℕ} (hKb : 0 < Kb) (gap : ℕ → ℝ)
    (h i : ℕ) (hhi : h ≤ i) (hgap0 : 0 ≤ gap i) (hgap : gap i ≤ g.width h)
    (top : ι) (htop : top ∈ tops)
    (he : g.eligible (g.rootWidth/B^2) (w/(T top).length) (i+1))
    (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 : ℝ × ℝ) :
    let weight := fun t x => (T t).weight Kw D x
…

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