WeightedAmplitudeMotion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Summation by parts for moving packet amplitudes. The unweighted interval motion and the endpoint-weight motion are charged separately.

theorem OAI.LipschitzHilbert.weighted_interval_motion line 15

theorem OAI.LipschitzHilbert.SourceLabeledLattice.stopping_amplitude_motion line 49

Source documentation

Motion of all original intervals controls the stopped source sum. The unitary may be the common diagonal carrier on the reference line.

theorem stopping_amplitude_motion (P : SourceLabeledLattice N κ Label Item)
    (coeff coeff' : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (jet : Fin 3) (stop : Fin N → ℕ) (hstop : Antitone stop)
    (start M : ℕ) (hstart : start ≤ M) (hmax : ∀ j, stop j ≤ M)
    (w w' : ℕ → ℂ) (x0 y0 x1 y1 A D B ε : ℝ)
    (U : EuclideanSpace ℂ κ →ₗᵢ[ℂ] EuclideanSpace ℂ κ)
    (hB : 0 ≤ B) (hε : 0 ≤ ε)
    (hweight : ‖w' M‖+(∑ j ∈ Finset.Ico start M, ‖w' (j+1)-w' j‖) ≤ A)
    (hweightdiff : ‖w' M-w M‖+
      (∑ j ∈ Finset.Ico start M, ‖(w' (j+1)-w (j+1))-(w' j-w j)‖) ≤ D)
    (hinterval : ∀ l u, l ≤ u → u ≤ N → ‖P.rawInterval coeff jet l u x0 y0‖ ≤ B)
    (hmotion : ∀ l u, l ≤ u → u ≤ N →
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice