SourcePredictionMotion.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Mass rescaling and block-transition motion for the snapshot prediction. Every estimate is relative to the positive snapshot masses; no positive lower cutoff is imposed on a mass.

def OAI.LipschitzHilbert.massPowerScale line 14
theorem OAI.LipschitzHilbert.massPowerScale_pos line 16
theorem OAI.LipschitzHilbert.massPowerScale_exp line 19
theorem OAI.LipschitzHilbert.massPowerScale_relative_motion line 25
theorem OAI.LipschitzHilbert.positive_relative_motion_to_sub line 51
theorem OAI.LipschitzHilbert.complex_relative_motion_to_sub line 57

theorem OAI.LipschitzHilbert.scalar_rescaling_motion line 68

Source documentation

The scalar and vector errors are kept separate until the final product. The reference vector may already have been rotated by a diagonal isometry.

theorem scalar_rescaling_motion {s s' c q η C : ℝ}
    (hs : 0 < s) (hs' : 0 ≤ s') (_hc : 0 ≤ c) (hq : 0 ≤ q)
    (_hη : 0 ≤ η) (_hC : 0 ≤ C) (hscale : |s'/s-1| ≤ q)
    (v' v : E) (hv : ‖v‖ ≤ C*c) (hmotion : ‖v'-v‖ ≤ η*c) :
    ‖s' • v'-s • v‖ ≤ ((1+q)*η+q*C)*s*c := by
…

theorem OAI.LipschitzHilbert.massPowerScale_amplitude_motion line 88
theorem OAI.LipschitzHilbert.prediction_mass_scale_identity line 104
Source documentation
The scalar in pred:scaled-motion times the snapshot child mass.
```
theorem prediction_mass_scale_identity {n c : ℝ} (hn : 0 < n) (hc : 0 < c)
    (p μ : ℝ) :
    massPowerScale n c (-(1/p)) (μ-1+1/p)*c = (c/n)^(1/p)*c^μ := by
…
```
Mentions: OAI.LipschitzHilbert.massPowerScale
theorem OAI.LipschitzHilbert.prediction_numerator_scale_identity line 119
theorem OAI.LipschitzHilbert.complex_product_relative_motion line 124
theorem OAI.LipschitzHilbert.complex_coefficient_amplitude_motion line 145

theorem OAI.LipschitzHilbert.prediction_numerator_motion line 169

Source documentation

The numerator rescaling in pred:numerator-motion. Its coefficient is expressed relative to n^μ*(c/n), exactly the snapshot parent scale times the child fraction.

theorem prediction_numerator_motion {n n' c δ qlam η C : ℝ}
    (hn : 0 < n) (hn' : 0 < n') (hc : 0 ≤ c) (hδ : 0 ≤ δ)
    (hqlam : 0 ≤ qlam) (hη : 0 ≤ η) (hC : 0 ≤ C)
    (hN : |Real.log n'-Real.log n| ≤ δ) (μ : ℝ)
    (lam lam' : ℂ) (hlam : ‖lam‖ ≤ 1) (hlammove : ‖lam'-lam‖ ≤ qlam)
    (v' v : E) (hv : ‖v‖ ≤ C*c) (hmotion : ‖v'-v‖ ≤ η*c) :
    let qn := Real.exp (|μ-1| * δ)*(|μ-1| * δ)
…

theorem OAI.LipschitzHilbert.AngularGrid.source_path_product_ne_zero line 204
theorem OAI.LipschitzHilbert.AngularGrid.source_path_product_norm_le_one line 215

theorem OAI.LipschitzHilbert.AngularGrid.source_scaled_prediction_motion line 238

Source documentation

Actual parent and child submasses supply the scalar part of pred:scaled-motion; the vector error is the already proved physical amplitude motion. The chosen boundary ancestor may precede the block.

theorem source_scaled_prediction_motion {ι E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    (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)
    (parentSet childSet : Finset ι) (hsub : childSet ⊆ parentSet)
    (hne : childSet.Nonempty)
    (hparent : parentSet ⊆ g.boundaryTops tops (fun t => (T t).slope)
      (fun t => w/(T t).length) (g.rootWidth/B^2) base i gap s)
…

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

theorem OAI.LipschitzHilbert.AngularGrid.source_block_transition_relative_motion line 297

Source documentation

The actual finite source transition product has relative motion obtained from physical child and boundary masses, without any mass cutoff.

theorem source_block_transition_relative_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)
    {Kb : ℕ} (hKb : 0 < Kb) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
    (h lower upper : ℕ) (hbase : h ≤ lower)
    (hgap : ∀ j ∈ Finset.Ico lower upper, 0 ≤ gap j ∧ gap j ≤ g.width h)
    (top : ι) (htop : top ∈ tops)
    (he : g.eligible (g.rootWidth/B^2) (w/(T top).length) upper)
    (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