DifferentialBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative bounds for the differential update

The vectors v, v1, and v2 stand for a field and its first and second directional derivatives. The operators K, K1, and K2 stand for the inverse transpose and its directional derivatives. Their stated bounds are used directly, with an arbitrary real-valued dual-size function. The algebra does not assume the desired increment or recurrence estimates.

theorem OAI.RegularPointCoordinates.differential_first_increment_norm_le line 22

Source documentation

The first derivative increment has the square-root forcing bound.

theorem differential_first_increment_norm_le
    (K K1 : E →L[ℝ] F) (dual : E → ℝ) (v v1 : E)
    {C epsilon q r z energy : ℝ} (hC : 1 ≤ C) (hq : 0 < q) (hr : 0 < r)
    (hK : ∀ w, ‖K w‖ ≤ C * dual w)
    (hK1 : ∀ w, ‖K1 w‖ ≤ C * q / r * dual w)
    (hv : dual v ≤ C * Real.sqrt epsilon * r * Real.sqrt energy)
    (hv1 : dual v1 ≤ C * Real.sqrt epsilon *
      (Real.sqrt z + Real.sqrt energy * q)) :
    ‖K v1 + K1 v‖ ≤ C ^ 2 * Real.sqrt epsilon *
      (Real.sqrt z + 2 * Real.sqrt energy * q) := by
…

theorem OAI.RegularPointCoordinates.differential_first_increment_sq_le line 47

Source documentation

The squared first increment in re:squared-increment.

theorem differential_first_increment_sq_le
    (K K1 : E →L[ℝ] F) (dual : E → ℝ) (v v1 : E)
    {C epsilon q r z energy : ℝ} (hC : 1 ≤ C)
    (hepsilon : 0 ≤ epsilon) (hq : 0 < q) (hr : 0 < r)
    (hz : 0 ≤ z) (henergy : 0 ≤ energy)
    (hK : ∀ w, ‖K w‖ ≤ C * dual w)
    (hK1 : ∀ w, ‖K1 w‖ ≤ C * q / r * dual w)
    (hv : dual v ≤ C * Real.sqrt epsilon * r * Real.sqrt energy)
    (hv1 : dual v1 ≤ C * Real.sqrt epsilon *
      (Real.sqrt z + Real.sqrt energy * q)) :
    ‖K v1 + K1 v‖ ^ 2 ≤ 5 * C ^ 4 * epsilon * (z + energy * q ^ 2) := by
…

theorem OAI.RegularPointCoordinates.differential_second_increment_norm_le line 79

Source documentation

Before rescaling, the three second-derivative terms are controlled by the same forcing.

theorem differential_second_increment_norm_le
    (K K1 K2 : E →L[ℝ] F) (dual : E → ℝ) (v v1 v2 : E)
    {C epsilon q r z energy : ℝ} (hC : 1 ≤ C)
    (hepsilon : 0 ≤ epsilon) (hepsilon1 : epsilon ≤ 1)
    (hq : 0 < q) (hr : 0 < r)
    (hK : ∀ w, ‖K w‖ ≤ C * dual w)
    (hK1 : ∀ w, ‖K1 w‖ ≤ C * q / r * dual w)
    (hK2 : ∀ w, ‖K2 w‖ ≤ C * q ^ 2 / r ^ 2 * dual w)
    (hv : dual v ≤ C * Real.sqrt epsilon * r * Real.sqrt energy)
    (hv1 : dual v1 ≤ C * Real.sqrt epsilon *
      (Real.sqrt z + Real.sqrt energy * q))
    (hv2 : dual v2 ≤ C / r * (Real.sqrt z * q + Real.sqrt energy * q ^ 2)) :
…

theorem OAI.RegularPointCoordinates.differential_second_increment_normalized_le line 132

Source documentation

The dyadic normalization of the actual second increment.

theorem differential_second_increment_normalized_le
    (K K1 K2 : E →L[ℝ] F) (dual : E → ℝ) (v v1 v2 : E)
    {C epsilon q r z energy : ℝ} (hC : 1 ≤ C)
    (hepsilon : 0 ≤ epsilon) (hepsilon1 : epsilon ≤ 1)
    (hq : 0 < q) (hr : 0 < r)
    (hK : ∀ w, ‖K w‖ ≤ C * dual w)
    (hK1 : ∀ w, ‖K1 w‖ ≤ C * q / r * dual w)
    (hK2 : ∀ w, ‖K2 w‖ ≤ C * q ^ 2 / r ^ 2 * dual w)
    (hv : dual v ≤ C * Real.sqrt epsilon * r * Real.sqrt energy)
    (hv1 : dual v1 ≤ C * Real.sqrt epsilon *
      (Real.sqrt z + Real.sqrt energy * q))
    (hv2 : dual v2 ≤ C / r * (Real.sqrt z * q + Real.sqrt energy * q ^ 2)) :
…

theorem OAI.RegularPointCoordinates.diagonal_recurrence_of_increment_bound line 157

Source documentation

Increasing the directional metric and halving the radius give the contractive half of the diagonal recurrence.

theorem diagonal_recurrence_of_increment_bound (old increment next : F)
    {q qnext r forcing : ℝ} (hq : 0 < q) (hr : 0 < r) (hmetric : q ≤ qnext)
    (hnext : next = old + increment)
    (hincrement : r / (2 * q) * ‖increment‖ ≤ forcing) :
    (r / 2) / qnext * ‖next‖ ≤ (r / q * ‖old‖) / 2 + forcing := by
…

theorem OAI.RegularPointCoordinates.differential_diagonal_update_recurrence line 174

Source documentation

The complete diagonal recurrence for an update with the actual three-term second derivative increment.

theorem differential_diagonal_update_recurrence
    (K K1 K2 : E →L[ℝ] F) (dual : E → ℝ) (v v1 v2 : E) (old next : F)
    {C epsilon q qnext r z energy : ℝ} (hC : 1 ≤ C)
    (hepsilon : 0 ≤ epsilon) (hepsilon1 : epsilon ≤ 1)
    (hq : 0 < q) (hr : 0 < r) (hmetric : q ≤ qnext)
    (hK : ∀ w, ‖K w‖ ≤ C * dual w)
    (hK1 : ∀ w, ‖K1 w‖ ≤ C * q / r * dual w)
    (hK2 : ∀ w, ‖K2 w‖ ≤ C * q ^ 2 / r ^ 2 * dual w)
    (hv : dual v ≤ C * Real.sqrt epsilon * r * Real.sqrt energy)
    (hv1 : dual v1 ≤ C * Real.sqrt epsilon *
      (Real.sqrt z + Real.sqrt energy * q))
    (hv2 : dual v2 ≤ C / r * (Real.sqrt z * q + Real.sqrt energy * q ^ 2))
…