CovariantLineMotion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Demodulated line motion from the horizontal derivative and vertical covariant derivative. The carrier frequencies do not enter the bound.

theorem OAI.LipschitzHilbert.diagonalModulation_sub line 17
theorem OAI.LipschitzHilbert.modulation_difference_norm line 24

theorem OAI.LipschitzHilbert.covariant_line_motion line 47

Source documentation

The two coordinate segments suffice, so no bound on a mixed partial derivative is needed.

theorem covariant_line_motion (F : ℝ → ℝ → EuclideanSpace ℂ κ) (frequency : κ → ℝ)
    (x0 x1 y0 y1 Cx Cy : ℝ)
    (hx : ∀ t ∈ uIcc x0 x1, DifferentiableAt ℝ (fun x => F x y1) t)
    (hy : ∀ t ∈ uIcc y0 y1, ∀ k, DifferentiableAt ℝ (fun y => F x0 y k) t)
    (hDx : ∀ t ∈ uIcc x0 x1, ‖deriv (fun x => F x y1) t‖ ≤ Cx)
    (hDy : ∀ t ∈ uIcc y0 y1,
      ‖covariantSignal frequency (fun k y => F x0 y k) t‖ ≤ Cy) :
    ‖F x1 y1 - diagonalModulation frequency (F x0 y0) (y1-y0)‖ ≤
      Cx*|x1-x0| + Cy*|y1-y0| := by
…

Mentions: OAI.LipschitzHilbert.covariantSignal