RadialCutoffChange.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Changing the local constant in a radial Sobolev residual

theorem OAI.RegularPointCoordinates.centered_radial_cutoff_change line 18

Source documentation

Two cutoff extensions of one produce the same local value and energy of the centered radial residual.

theorem centered_radial_cutoff_change {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (g eta chi : SobolevSpace μ hQ)
    (z b : Euclidean n) (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (hchi : SobolevSpace.toLp μ hQ chi =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ)) :
    let f := g - centeredAffineSobolev μ hQ u eta z b
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.centeredAffineSobolev