AngularMassMotion.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual source averaging scale makes every boundary submass move by order G^(-1/2), including submasses from other shifted blocks.

theorem OAI.LipschitzHilbert.source_mass_motion_budget line 16

Source documentation

The two locality terms are small on the manuscript's averaging cell. The stronger B² eligibility and width hypotheses retain a spare factor B.

theorem source_mass_motion_budget {rho child w B G gap a : ℝ}
    (_hrho : 0 < rho) (hchild : 0 < child) (hw : 0 < w)
    (hB : 1 ≤ B) (hG : 0 < G) (hgap : gap ≤ rho)
    (hblock : rho ≤ B*child) (ha : |a| ≤ w/(child*Real.sqrt G)) :
    (rho/(B^2*w)+(3*rho+gap)/(B^2*w))*|a| ≤ 5/Real.sqrt G := by
…

theorem OAI.LipschitzHilbert.AngularGrid.boundary_submass_source_motion line 46

Source documentation

At H=w/(child sqrt G), concrete boundary submasses have uniformly small logarithmic motion. Here the top width lower bound is exactly the consequence W=m w≥B²w used in the source.

theorem boundary_submass_source_motion (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)
    (base h i : ℕ) (hhi : h ≤ i) (gap : ℝ) (hgap0 : 0 ≤ gap) (hgap : gap ≤ g.width h)
    (s sR : ℝ) (hs : g.index h s = g.index h sR)
    (child : ℝ) (hchild : 0 < child) (hblock : g.width h ≤ B*child)
    (A : Finset ι) (hA : A.Nonempty)
    (hsub : A ⊆ g.boundaryTops tops (fun t => (T t).slope)
      (fun t => w/(T t).length) (g.rootWidth/B^2) base i gap s)
    (a : ℝ) (ha : |a| ≤ w/(child*Real.sqrt (g.branching:ℝ))) (z : ℝ × ℝ) :
    |Real.log (∑ t ∈ A, (T t).weight K D (SlopeBox.lineShift sR a z)) -
…

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

theorem OAI.LipschitzHilbert.positive_ratio_log_motion line 82

Source documentation

Moving numerator and denominator logarithms give the exact uniform bound needed for one child-to-boundary ratio.

theorem positive_ratio_log_motion {a b a' b' delta : ℝ}
    (ha : 0 < a) (hb : 0 < b) (ha' : 0 < a') (hb' : 0 < b')
    (hA : |Real.log a'-Real.log a| ≤ delta)
    (hB : |Real.log b'-Real.log b| ≤ delta) :
    |Real.log (a'/b')-Real.log (a/b)| ≤ 2*delta := by
…

theorem OAI.LipschitzHilbert.exponential_relative_motion line 95
Source documentation
A logarithmic perturbation of a nonzero exponential gives relative complex motion; the bound does not involve the original logarithm.
```
theorem exponential_relative_motion {a b : ℂ} {E : ℝ}
    (hE : 0 ≤ E) (hmove : ‖b-a‖ ≤ E) :
    ‖Complex.exp b/Complex.exp a-1‖ ≤ Real.exp E*E := by
…
```

theorem OAI.LipschitzHilbert.transition_product_relative_motion line 108

Source documentation

A finite product of transition exponentials depends only on the motion of its specified logarithms, never their magnitudes.

theorem transition_product_relative_motion {J : Type*} (s : Finset J)
    (phase : J → ℂ) (loss0 loss1 : J → ℝ) (Z delta : ℝ)
    (hZ : 0 ≤ Z) (hdelta : 0 ≤ delta)
    (hphase : ∀ j ∈ s, ‖phase j‖ ≤ Z)
    (hloss : ∀ j ∈ s, |loss1 j-loss0 j| ≤ delta) :
    ‖(∏ j ∈ s, Complex.exp (phase j*(loss1 j:ℂ))) /
        (∏ j ∈ s, Complex.exp (phase j*(loss0 j:ℂ))) - 1‖ ≤
      Real.exp ((s.card:ℝ)*Z*delta)*((s.card:ℝ)*Z*delta) := by
…

theorem OAI.LipschitzHilbert.AngularGrid.source_path_relative_motion line 132

Source documentation

The actual block transition product has small relative motion once its concrete child and boundary masses have the preceding local bounds.

theorem source_path_relative_motion {ι 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 : ℕ → ℂ)
    (lower upper : ℕ) (top : ι) (htop : top ∈ tops)
    (he : g.eligible cutoff (precision top) upper) (x0 x1 : X)
    (Z delta : ℝ) (hZ : 0 ≤ Z) (hdelta : 0 ≤ delta)
    (hphase : ∀ j ∈ Finset.Ico lower upper, ‖phase j‖ ≤ Z)
    (hmass : ∀ j ∈ Finset.Ico lower upper,
      |Real.log (g.mass tops slope precision cutoff weight (j+1) (g.index (j+1) (slope top)) x1) -
        Real.log (g.mass tops slope precision cutoff weight (j+1) (g.index (j+1) (slope top)) x0)| ≤ delta)
    (hboundary : ∀ j ∈ Finset.Ico lower upper,
…

Mentions: OAI.LipschitzHilbert.AngularGrid