TwoCenterRadialFits.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Subtracting the two actual radial fits in their common frame

theorem OAI.RegularPointCoordinates.averaged_energy_sub_le line 18

Source documentation

Local energy obeys the squared triangle estimate on an arbitrary common region, retaining its original normalization.

theorem averaged_energy_sub_le (Ω : Set X) (f g : SobolevSpace μ hQ) :
    (μ.real Ω)⁻¹ * (∫ x in Ω, localGamma μ hQ (f - g) (f - g) x ∂μ) ≤
      2 * ((μ.real Ω)⁻¹ * ∫ x in Ω, localGamma μ hQ f f x ∂μ) +
      2 * ((μ.real Ω)⁻¹ * ∫ x in Ω, localGamma μ hQ g g x ∂μ) := by
…

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

theorem OAI.RegularPointCoordinates.normalized_sobolev_sub_sq_le line 48
theorem OAI.RegularPointCoordinates.radial_difference_representative line 65
Source documentation
The difference of the two radial representatives represents the derivative of the difference of the two actual Poisson replacements.
```
theorem radial_difference_representative (Ω : Set X)
    (fz fx u gz gx : SobolevSpace μ hQ)
    (hz : SobolevSpace.toLp μ hQ gz =ᵐ[μ.restrict Ω] localGamma μ hQ fz u)
    (hx : SobolevSpace.toLp μ hQ gx =ᵐ[μ.restrict Ω] localGamma μ hQ fx u) :
    SobolevSpace.toLp μ hQ (gz - gx) =ᵐ[μ.restrict Ω] localGamma μ hQ (fz - fx) u := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.two_center_radial_fit_bounds line 80

Source documentation

Subtracting the common-frame fits produces the affine fit of the two-center derivative, with the original displacement constant.

theorem two_center_radial_fit_bounds {n : ℕ}
    (Ω : Set X) (hfin : μ Ω ≠ ∞) (η : SobolevSpace μ hQ)
    (U Gz Gx : Euclidean n →L[ℝ] SobolevSpace μ hQ)
    (Az Ax : Euclidean n →L[ℝ] Euclidean n) (c : Euclidean n →L[ℝ] ℝ)
    {Ez Ex Dz Dx : ℝ}
    (hzv : ∀ b, ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω
      (Gz b - U (Az b)))‖ ^ 2 ≤ Ez * ‖b‖ ^ 2)
    (hxv : ∀ b, ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω
      (Gx b - U (Ax b) + c b • η))‖ ^ 2 ≤ Ex * ‖b‖ ^ 2)
    (hze : ∀ b, (μ.real Ω)⁻¹ * (∫ x in Ω, localGamma μ hQ
      (Gz b - U (Az b)) (Gz b - U (Az b)) x ∂μ) ≤ Dz * ‖b‖ ^ 2)
    (hxe : ∀ b, (μ.real Ω)⁻¹ * (∫ x in Ω, localGamma μ hQ
…

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