NormalizedProjectionResidual.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Normalizing the actual orthogonal projection residual

theorem OAI.RegularPointCoordinates.normalized_projection_orthogonality line 19

Source documentation

Scaling a genuine projection residual preserves all affine orthogonality, including the constant term.

theorem normalized_projection_orthogonality {n : ℕ}
    (s : Set X) (hfin : μ s ≠ ∞) (u : Fin n → SobolevSpace μ hQ)
    (v w : SobolevSpace μ hQ)
    (hw : SobolevSpace.restrictLp μ hQ s w =
      affineResidual μ hQ u s hfin (SobolevSpace.restrictLp μ hQ s v))
    (a : ℝ) (j : Option (Fin n)) :
    ⟪localAffineMomentFamily μ hQ u (a • w) s hfin none,
      localAffineMomentFamily μ hQ u (a • w) s hfin (some j)⟫_ℝ = 0 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.affineResidual, OAI.RegularPointCoordinates.localAffineMomentFamily

theorem OAI.RegularPointCoordinates.normalized_residual_unit_moment line 48
Source documentation
Dividing by the nonzero inner mean norm makes the same residual's diagonal moment exactly one.
```
theorem normalized_residual_unit_moment {n : ℕ}
    (s : Set X) (hfin : μ s ≠ ∞) (u : Fin n → SobolevSpace μ hQ)
    (w : SobolevSpace μ hQ)
    (hpos : 0 < ‖normalizeLocalL2 μ s hfin (SobolevSpace.restrictLp μ hQ s w)‖) :
    let α := ‖normalizeLocalL2 μ s hfin (SobolevSpace.restrictLp μ hQ s w)‖
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp