ProjectedEulerIdentity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The Euler equation of the actual affine projection residual

theorem OAI.RegularPointCoordinates.localRadialDerivative_eq_of_euler line 20

Source documentation

The scalar equation obtained from Poincare is an equality in the same local L2 space as the radial derivative.

theorem localRadialDerivative_eq_of_euler (Ω : Set X)
    (f v η e : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B) (k : ℝ)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (he : localGamma μ hQ f v =ᵐ[μ.restrict Ω]
      fun x => SobolevSpace.toLp μ hQ v x + k + SobolevSpace.toLp μ hQ e x) :
    localRadialDerivative μ hQ Ω f hf v =
      SobolevSpace.restrictLp μ hQ Ω (v + k • η + e) := by
…

theorem OAI.RegularPointCoordinates.projected_euler_identity line 43

Source documentation

Subtracting the actual affine fit creates precisely the coefficient b-A b, the constant k+c, and the difference of the two known errors.

theorem projected_euler_identity {n : ℕ} (Ω : Set X)
    (f v η ev : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (U G : Euclidean n →L[ℝ] SobolevSpace μ hQ)
    (A : Euclidean n →L[ℝ] Euclidean n) (b : Euclidean n) (k c : ℝ)
    (hv : localRadialDerivative μ hQ Ω f hf v =
      SobolevSpace.restrictLp μ hQ Ω (v + k • η + ev))
    (hG : localRadialDerivative μ hQ Ω f hf (U b) =
      SobolevSpace.restrictLp μ hQ Ω (G b)) :
    let w := v - c • η - U b
…

theorem OAI.RegularPointCoordinates.projected_euler_error_bound line 70

Source documentation

The projected error remains linear in the two original errors, before any division by the residual norm.

theorem projected_euler_error_bound {n : ℕ} (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (ev : SobolevSpace μ hQ) (U G : Euclidean n →L[ℝ] SobolevSpace μ hQ)
    (A : Euclidean n →L[ℝ] Euclidean n) (b : Euclidean n) {E D : ℝ}
    (hev : ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω ev)‖ ≤ E)
    (hfit : ‖normalizeLocalL2 μ Ω hfin
      (SobolevSpace.restrictLp μ hQ Ω (G b - U (A b)))‖ ≤ D * ‖b‖) :
    ‖normalizeLocalL2 μ Ω hfin
      (SobolevSpace.restrictLp μ hQ Ω (ev - (G b - U (A b))))‖ ≤ E + D * ‖b‖ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp

theorem OAI.RegularPointCoordinates.projected_euler_coefficient_bound line 84

Source documentation

The forcing coefficients are controlled by the small inner residual and its radial derivative, rather than by the full size of the projection.

theorem projected_euler_coefficient_bound {n : ℕ} (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (f w η e : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (u : Fin n → SobolevSpace μ hQ) (N : Euclidean n ≃L[ℝ] Euclidean n)
    (ell : Euclidean n) (k : ℝ) {H α Cg Cw E : ℝ} (hH : 0 ≤ H)
    (hbound : ∀ c a, |c| + ‖N.symm a‖ ≤ H *
      ‖normalizeLocalL2 μ Ω hfin (affineCoordinateMap μ hQ u Ω hfin (c, a))‖)
    (heuler : localRadialDerivative μ hQ Ω f hf w = SobolevSpace.restrictLp μ hQ Ω
      (w + sobolevColumnMap μ hQ u ell + k • η + e))
    (hD : ‖normalizeLocalL2 μ Ω hfin (localRadialDerivative μ hQ Ω f hf w)‖ ≤ Cg * α)
    (hw : ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω w)‖ ≤ Cw * α)
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.affineCoordinateMap, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.sobolevColumnMap