CommutatorRepresentatives.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Independence of the chosen Sobolev gradient representatives

theorem OAI.RegularPointCoordinates.commutator_error_transfer line 17

Source documentation

The commutator estimate applies to the representatives selected by radial approximation, even when the Hessian construction chose others.

theorem commutator_error_transfer {Ω : Set X}
    (f v u g₀ h₀ g h : SobolevSpace μ hQ)
    (hg₀ : SobolevSpace.toLp μ hQ g₀ =ᵐ[μ.restrict Ω] localGamma μ hQ f u)
    (hh₀ : SobolevSpace.toLp μ hQ h₀ =ᵐ[μ.restrict Ω] localGamma μ hQ v u)
    (hg : SobolevSpace.toLp μ hQ g =ᵐ[μ.restrict Ω] localGamma μ hQ f u)
    (hh : SobolevSpace.toLp μ hQ h =ᵐ[μ.restrict Ω] localGamma μ hQ v u)
    {D : ℝ}
    (herror : (∫ x in Ω, (localGamma μ hQ v g₀ x - localGamma μ hQ f h₀ x -
      localGamma μ hQ v u x) ^ 2 ∂μ) ≤ D) :
    (∫ x in Ω, (localGamma μ hQ v g x - localGamma μ hQ f h x -
      localGamma μ hQ v u x) ^ 2 ∂μ) ≤ D := by
…

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