RawCutoffError.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Directional cutoff error outside the controlled normalization range

theorem OAI.RegularPointCoordinates.cutoff_direction_error_le_raw line 21

Source documentation

A raw gradient bound gives a global cutoff error budget after any linear change of frame. No regularity is required outside the cutoff.

theorem cutoff_direction_error_le_raw (U : E →L[ℝ] SobolevSpace μ hQ)
    (A : E →L[ℝ] E) {s : Set X} (hsfin : μ s ≠ ∞)
    {χ : X → ℝ} (hχ : Continuous χ)
    (hχrange : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1) (hχzero : ∀ x ∉ s, χ x = 0)
    {L B : ℝ} (hL : 0 ≤ L)
    (hgradient : ∀ v : E, ∀ᵐ x ∂μ.restrict s,
      localGamma μ hQ (U v) (U v) x ≤ L * ‖v‖ ^ 2)
    (hframe : ∀ v : E, ‖A v‖ ^ 2 ≤ B * ‖v‖ ^ 2) (v : E) :
    (∫ x, χ x * |localGamma μ hQ (U (A v)) (U (A v)) x - ‖v‖ ^ 2| ∂μ) ≤
      (L * B + 1) * μ.real s * ‖v‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma