NormalizedDirectionError.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Directional Gram errors after changing the exact normalizing frame

theorem OAI.RegularPointCoordinates.integral_abs_sub_const_le line 20

Source documentation

Shifting the constant in an L1 error costs the measure times the shift.

theorem integral_abs_sub_const_le {f : X → ℝ} {s : Set X}
    (hf : IntegrableOn f s μ) (hs : μ s ≠ ∞) (a b : ℝ) :
    (∫ x in s, |f x - b| ∂μ) ≤
      (∫ x in s, |f x - a| ∂μ) + μ.real s * |a - b| := by
…

theorem OAI.RegularPointCoordinates.changed_frame_norm_sq line 35

Source documentation

Express the length in the local exact frame using the working-frame mean.

theorem changed_frame_norm_sq {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (p : X) (r : ℝ)
    (S : Euclidean n ≃L[ℝ] Euclidean n) (A : Euclidean n →L[ℝ] Euclidean n)
    (hexact : IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u)
      (ball p r) measurableSet_ball S) (v : Euclidean n) :
    ‖S.symm (A v)‖ ^ 2 =
      ⟪v, sobolevMeanGram μ hQ ((sobolevColumnMap μ hQ u).comp A)
        (ball p r) measurableSet_ball v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.sobolevMeanGram

theorem OAI.RegularPointCoordinates.changed_frame_local_error line 49

Source documentation

The first-order splitting estimate expressed in arbitrary coordinates.

theorem changed_frame_local_error {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (p : X) (r : ℝ)
    (S : Euclidean n ≃L[ℝ] Euclidean n) (A : Euclidean n →L[ℝ] Euclidean n)
    {ε : ℝ} {w : X → Euclidean n} (hε : 0 ≤ ε)
    (hfirst : FirstOrderSplittingOn μ hQ p r ε (transformedColumn μ hQ u S) w)
    (hvolume : 0 < μ.real (ball p r)) (hfinite : μ (ball p r) ≠ ∞)
    (v : Euclidean n) :
    (∫ x in ball p r, |localGamma μ hQ (sobolevColumnMap μ hQ u (A v))
      (sobolevColumnMap μ hQ u (A v)) x - ‖S.symm (A v)‖ ^ 2| ∂μ) ≤
      (n : ℝ) ^ 2 * (ε * μ.real (ball p r)) * ‖S.symm (A v)‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.changed_frame_directional_error line 73

Source documentation

An exact frame on the current ball and an operator estimate for the working frame give the L1 directional error needed in a Gaussian shell.

theorem changed_frame_directional_error {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (p : X) (r : ℝ)
    (S : Euclidean n ≃L[ℝ] Euclidean n) (A : Euclidean n →L[ℝ] Euclidean n)
    {ε δ : ℝ} {w : X → Euclidean n} (hε : 0 ≤ ε)
    (hfirst : FirstOrderSplittingOn μ hQ p r ε (transformedColumn μ hQ u S) w)
    (hexact : IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u)
      (ball p r) measurableSet_ball S)
    (hvolume : 0 < μ.real (ball p r)) (hfinite : μ (ball p r) ≠ ∞)
    (hnorm : ‖sobolevMeanGram μ hQ ((sobolevColumnMap μ hQ u).comp A)
      (ball p r) measurableSet_ball - ContinuousLinearMap.id ℝ (Euclidean n)‖ ≤ δ)
    (v : Euclidean n) :
    (∫ x in ball p r, |localGamma μ hQ (sobolevColumnMap μ hQ u (A v))
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.localGamma