AffineProjection.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The actual `L²` projection onto the affine coordinate span

def OAI.RegularPointCoordinates.restrictedOne line 18
def OAI.RegularPointCoordinates.affineCoordinateMap line 23
Source documentation
Constants and linear combinations of the given coordinates, restricted as actual L² functions on the testing set.
```
def affineCoordinateMap : (ℝ × Euclidean n) →L[ℝ] Lp ℝ 2 (μ.restrict s) :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.affineCoordinateMap_apply line 28
def OAI.RegularPointCoordinates.affineCoordinateSpace line 33
instance OAI.RegularPointCoordinates.affineCoordinateSpace_finiteDimensional line 36
def OAI.RegularPointCoordinates.affineProjection line 42
Source documentation
The least-squares affine fit exists without assuming independence of its generators. Coefficient uniqueness can be added after normalization.
```
def affineProjection : Lp ℝ 2 (μ.restrict s) →L[ℝ] Lp ℝ 2 (μ.restrict s) :=
…
```
theorem OAI.RegularPointCoordinates.affineProjection_has_coefficients line 45
theorem OAI.RegularPointCoordinates.affineProjection_orthogonal line 53
theorem OAI.RegularPointCoordinates.affineProjection_best line 61
Source documentation
The affine fit minimizes the L² error among all coordinate-affine functions, with the unnormalized integral convention.
```
theorem affineProjection_best (f : Lp ℝ 2 (μ.restrict s))
    (c : ℝ) (v : Euclidean n) :
    ‖f - affineProjection μ hQ u s hfin f‖ ≤
      ‖f - affineCoordinateMap μ hQ u s hfin (c, v)‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.affineProjection, OAI.RegularPointCoordinates.affineCoordinateMap
def OAI.RegularPointCoordinates.affineResidual line 78
Source documentation
The residual is a bounded linear map, so all scalar directional fits can be assembled linearly before taking their matrix coefficients.
```
def affineResidual : Lp ℝ 2 (μ.restrict s) →L[ℝ] Lp ℝ 2 (μ.restrict s) :=
…
```
theorem OAI.RegularPointCoordinates.affineResidual_norm_le line 81
theorem OAI.RegularPointCoordinates.affineProjection_norm_le line 89
theorem OAI.RegularPointCoordinates.affineResidual_integral line 95
Source documentation
Orthogonality to constants is the vanishing of the actual integral, including when the original ambient measure is infinite.
```
theorem affineResidual_integral (f : Lp ℝ 2 (μ.restrict s)) :
    ∫ x, affineResidual μ hQ u s hfin f x ∂μ.restrict s = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.affineResidual
theorem OAI.RegularPointCoordinates.affineResidual_coordinate_inner line 111
Source documentation
The residual is orthogonal to each original coordinate in L².
```
theorem affineResidual_coordinate_inner (f : Lp ℝ 2 (μ.restrict s)) (i : Fin n) :
    ⟪affineResidual μ hQ u s hfin f,
      SobolevSpace.restrictLp μ hQ s (u i)⟫_ℝ = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.affineResidual, OAI.RegularPointCoordinates.SobolevSpace.restrictLp

theorem OAI.RegularPointCoordinates.affineProjection_controlled_coefficients line 122

Source documentation

Uniform nondegeneracy of the value coordinates gives uniform bounds for the coefficients of their least-squares fit.

theorem affineProjection_controlled_coefficients (f : Lp ℝ 2 (μ.restrict s))
    {C : ℝ} (hC : 0 ≤ C)
    (hbound : ∀ c v, |c| + ‖v‖ ≤ C * ‖affineCoordinateMap μ hQ u s hfin (c, v)‖) :
    ∃ c : ℝ, ∃ v : Euclidean n,
      affineProjection μ hQ u s hfin f = affineCoordinateMap μ hQ u s hfin (c, v) ∧
      |c| + ‖v‖ ≤ C * ‖f‖ := by
…

Mentions: OAI.RegularPointCoordinates.affineCoordinateMap, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.affineProjection

theorem OAI.RegularPointCoordinates.affineResidual_eq_zero_of_mem line 139
Source documentation
Vanishing of an affine residual follows from affinity itself. This is the final contradiction after Euclidean Euler rigidity in sharp projection.
```
theorem affineResidual_eq_zero_of_mem (f : Lp ℝ 2 (μ.restrict s))
    (hf : f ∈ affineCoordinateSpace μ hQ u s hfin) :
    affineResidual μ hQ u s hfin f = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.affineCoordinateSpace, OAI.RegularPointCoordinates.affineResidual

OAI/Geometry/RCD/Harmonic/AffineProjection.lean

The actual L² projection onto the affine coordinate span

`OAI/Geometry/RCD/Harmonic/AffineProjection.lean`

The actual `L²` projection onto the affine coordinate span