CarrierSlopeMotion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Replacing a top's carrier by its angular child-center carrier costs only the child width, not the width of an earlier block ancestor.

theorem OAI.LipschitzHilbert.diagonalModulation_change_slope line 14

theorem OAI.LipschitzHilbert.carrier_replacement_motion line 27

Source documentation

A bound in the top carrier transfers to the one common child carrier.

theorem carrier_replacement_motion (frequency : κ → ℝ)
    (v0 v1 : EuclideanSpace ℂ κ) (F B E : ℝ) (hF : 0 ≤ F)
    (hfrequency : ∀ k, |frequency k| ≤ F) (hB : ‖v0‖ ≤ B)
    (reference top center b : ℝ)
    (hmotion : ‖v1-diagonalModulation frequency v0 ((reference-top)*b)‖ ≤ E) :
    ‖v1-diagonalModulation frequency v0 ((reference-center)*b)‖ ≤
      E+F*B*|top-center| * |b| := by
…

theorem OAI.LipschitzHilbert.source_carrier_replacement_budget line 44

Source documentation

At the source averaging scale the carrier replacement is of order G^(-1/2), uniformly in the absolute frequency center.

theorem source_carrier_replacement_budget {F C w rho G d b : ℝ}
    (_hF : 0 ≤ F) (hC : 0 ≤ C) (hw : 0 < w) (hrho : 0 < rho) (hG : 0 < G)
    (hfrequency : F ≤ C/w) (hslope : |d| ≤ rho)
    (hdisplacement : |b| ≤ w/(rho*Real.sqrt G)) :
    F*|d| * |b| ≤ C/Real.sqrt G := by
…