OAI/Analysis/LipschitzHilbert/Phase/SourcePredictableAmplitudeMotion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.AngularGrid.source_single_top_predictable_motion line 20

   Source documentation

   The per-top estimate retains four powers of the snapshot weight. Only the unweighted interval estimate is an input; the weight motion is derived from the physical geometry.

   theorem source_single_top_predictable_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 start M : ℕ) (hstart : start ≤ M) (hbase : h ≤ start)
       (hgap : ∀ j, h ≤ j → j ≤ M → 0 ≤ gap j ∧ gap j ≤ g.width h)
       (top : ι) (htop : top ∈ tops)
       (he : g.eligible (g.rootWidth/B^2) (w/(T top).length) M)
       (sR : ℝ) (hs : g.index h (T top).slope = g.index h sR)
       (child : ℝ) (hchild : 0 < child) (hblock : g.width h ≤ B*child)
       (b : ℝ) (hb : |b| ≤ w/(child*Real.sqrt (g.branching:ℝ))) (z : ℝ × ℝ)
   …

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

2. theorem OAI.LipschitzHilbert.AngularGrid.source_node_predictable_motion line 122

   Source documentation

   The complete family of actual packets has motion proportional to the mass of its angular node, independently of the number of tops.

   theorem source_node_predictable_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 start : ℕ) (hbase : h ≤ start) (M : ι → ℕ)
       (hM : ∀ t ∈ tops, g.eligible (g.rootWidth/B^2) (w/(T t).length) (M t))
       (hMmax : ∀ t ∈ tops, ∀ j, g.eligible (g.rootWidth/B^2) (w/(T t).length) j → j ≤ M t)
       (hgap : ∀ t ∈ tops, ∀ j, h ≤ j → j ≤ M t → 0 ≤ gap j ∧ gap j ≤ g.width h)
       (sR : ℝ) (cell : ℤ) (hs : ∀ t ∈ g.cellTops tops (fun t => (T t).slope)
         (fun t => w/(T t).length) (g.rootWidth/B^2) start cell,
         g.index h (T t).slope = g.index h sR)
   …

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