OAI/Analysis/LipschitzHilbert/Trees/SourceShiftedCellMotion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.AngularGrid.shiftedPathLossTops line 16
2. theorem OAI.LipschitzHilbert.AngularGrid.shiftedPathLossTops_subset line 26
3. theorem OAI.LipschitzHilbert.AngularGrid.shiftedPathMass_difference line 37
4. theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_absolute_motion line 57

   Source documentation

   Parent mass and absolute loss have the same relative motion bound: each is a positive sum over a subset of the parent tops.

   theorem source_shifted_absolute_motion {ι : Type*} {K : ℕ}
       (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)
       (hK : 0 < K) (σ : Fin K) (j : ℕ) (top : ι)
       (he : g.eligible (g.rootWidth/B^2) (w/(T top).length) (ShiftedBlocks.endpoint σ j))
       (sR : ℝ) (hs : g.index (ShiftedBlocks.endpoint σ j) (T top).slope =
         g.index (ShiftedBlocks.endpoint σ j) sR)
       (hblock : g.width (ShiftedBlocks.endpoint σ j) ≤ B*g.width (ShiftedBlocks.endpoint σ (j+1)))
       (b : ℝ) (hb : |b| ≤ w/(g.width (ShiftedBlocks.endpoint σ (j+1))*Real.sqrt (g.branching:ℝ)))
       (z : ℝ × ℝ) :
       let n := fun x => g.shiftedPathMass tops (fun t => (T t).slope)
   …

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

5. theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_line_cell_motion line 112

   Source documentation

   Every pair of physical points in one reference cell has the above motion bound. This is uniform over cells and their position on the line.

   theorem source_shifted_line_cell_motion {ι : Type*} {K : ℕ}
       (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)
       (hK : 0 < K) (σ : Fin K) (j : ℕ) (top : ι)
       (he : g.eligible (g.rootWidth/B^2) (w/(T top).length) (ShiftedBlocks.endpoint σ j))
       (sR y : ℝ) (hs : g.index (ShiftedBlocks.endpoint σ j) (T top).slope =
         g.index (ShiftedBlocks.endpoint σ j) sR)
       (hblock : g.width (ShiftedBlocks.endpoint σ j) ≤ B*g.width (ShiftedBlocks.endpoint σ (j+1)))
       (grid : FiniteLineGrid)
       (hgrid : grid.width ≤ w/(g.width (ShiftedBlocks.endpoint σ (j+1))*Real.sqrt (g.branching:ℝ)))
       (x z : ℝ) (hx : x ∈ grid.root) (hz : z ∈ grid.root) :
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.AngularGrid.width, OAI.LipschitzHilbert.ShiftedBlocks.endpoint, OAI.LipschitzHilbert.FiniteLineGrid