LocalAffineCutoff.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A common cutoff for local affine radial residuals

theorem OAI.RegularPointCoordinates.local_cutoff_restrict_eq line 19

Source documentation

Two local representatives of the constant one have identical restrictions.

theorem local_cutoff_restrict_eq (Ω : Set X) (η ζ : SobolevSpace μ hQ)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (hζ : SobolevSpace.toLp μ hQ ζ =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ)) :
    SobolevSpace.restrictLp μ hQ Ω η = SobolevSpace.restrictLp μ hQ Ω ζ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.restrictLp

theorem OAI.RegularPointCoordinates.local_affine_cutoff_errors line 29

Source documentation

Replacing the compact extension of an affine constant preserves both the normalized value error and the local gradient energy of its residual.

theorem local_affine_cutoff_errors (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (q η ζ : SobolevSpace μ hQ) (c : ℝ)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (hζ : SobolevSpace.toLp μ hQ ζ =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ)) :
    normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (q - c • η)) =
      normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (q - c • ζ)) ∧
    (∫ x in Ω, localGamma μ hQ (q - c • η) (q - c • η) x ∂μ) =
      ∫ x in Ω, localGamma μ hQ (q - c • ζ) (q - c • ζ) x ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.localGamma