RadialFitRestriction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Restricting the value and energy bounds of an actual radial fit

theorem OAI.RegularPointCoordinates.normalized_fit_restrict_sq line 20

Source documentation

A normalized squared value error only pays the actual volume ratio when the common commutator ball is smaller than the radial fitting ball.

theorem normalized_fit_restrict_sq {s t : Set X} (hts : t ⊆ s)
    (hs : μ s ≠ ∞) (ht : μ t ≠ ∞) (hs0 : 0 < μ.real s) (ht0 : 0 < μ.real t)
    (f : SobolevSpace μ hQ) {C E : ℝ} (hE : 0 ≤ E)
    (hvol : μ.real s ≤ C * μ.real t)
    (hfit : ‖normalizeLocalL2 μ s hs (SobolevSpace.restrictLp μ hQ s f)‖ ^ 2 ≤ E) :
    ‖normalizeLocalL2 μ t ht (SobolevSpace.restrictLp μ hQ t f)‖ ^ 2 ≤ C * E := by
…

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

theorem OAI.RegularPointCoordinates.normalized_fit_energy_restrict line 32

Source documentation

The identical volume-ratio loss applies to the squared gradient error.

theorem normalized_fit_energy_restrict {s t : Set X} (hts : t ⊆ s)
    (hs0 : 0 < μ.real s) (ht0 : 0 < μ.real t)
    (f : SobolevSpace μ hQ) {C E : ℝ} (hE : 0 ≤ E)
    (hvol : μ.real s ≤ C * μ.real t)
    (hfit : (μ.real s)⁻¹ * (∫ x in s, localGamma μ hQ f f x ∂μ) ≤ E) :
    (μ.real t)⁻¹ * (∫ x in t, localGamma μ hQ f f x ∂μ) ≤ C * E := by
…

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