LinearRadialFits.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Linear assembly of the actual centered radial fits

def OAI.RegularPointCoordinates.finiteCoefficientMap line 16
Source documentation
The original affine coefficients, extended linearly from basis rows.
```
def finiteCoefficientMap {n : ℕ} (coeff : Fin n → Euclidean n) :
    Euclidean n →L[ℝ] Euclidean n :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.finiteCoefficientMap_apply line 20
theorem OAI.RegularPointCoordinates.finiteCoefficientMap_single line 24
def OAI.RegularPointCoordinates.centeredSobolevMap line 33
Source documentation
Centering preserves the linear dependence on the affine covector.
```
def centeredSobolevMap {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (η : SobolevSpace μ hQ) (v : Euclidean n) : Euclidean n →L[ℝ] SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.centeredSobolevMap_apply line 38
theorem OAI.RegularPointCoordinates.centered_radial_residual_column line 48
Source documentation
Combining centered row fits is exactly the centered fit with the combined coefficient, so the value and gradient estimates use one residual.
```
theorem centered_radial_residual_column {n : ℕ}
    (u g : Fin n → SobolevSpace μ hQ) (η : SobolevSpace μ hQ) (v : Euclidean n)
    (coeff : Fin n → Euclidean n) (b : Euclidean n) :
    sobolevColumnMap μ hQ (fun j => g j - centeredAffineSobolev μ hQ u η v (coeff j)) b =
      sobolevColumnMap μ hQ g b - centeredAffineSobolev μ hQ u η v (finiteCoefficientMap coeff b) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.centeredAffineSobolev, OAI.RegularPointCoordinates.finiteCoefficientMap

theorem OAI.RegularPointCoordinates.linear_centered_radial_bounds line 64

Source documentation

All rowwise W12 bounds from the actual dyadic radial construction extend to every covector with the same combined affine coefficient.

theorem linear_centered_radial_bounds {n : ℕ}
    (u g : Fin n → SobolevSpace μ hQ) (η : SobolevSpace μ hQ) (v : Euclidean n)
    (coeff : Fin n → Euclidean n) (Ω Ω' : Set X) (hfin : μ Ω ≠ ∞) {E D : ℝ} (hE : 0 ≤ E)
    (hvalue : ∀ j, ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω
      (g j - centeredAffineSobolev μ hQ u η v (coeff j)))‖ ^ 2 ≤ E)
    (henergy : ∀ j, (∫ x in Ω', localGamma μ hQ
      (g j - centeredAffineSobolev μ hQ u η v (coeff j))
      (g j - centeredAffineSobolev μ hQ u η v (coeff j)) x ∂μ) ≤ D)
    (b : Euclidean n) :
    let R := sobolevColumnMap μ hQ g b - centeredAffineSobolev μ hQ u η v (finiteCoefficientMap coeff b)
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.centeredAffineSobolev, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.finiteCoefficientMap