HomogeneousAffineImprovement.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Removing the unit-norm restriction in harmonic affine improvement

theorem OAI.RegularPointCoordinates.harmonicTargetNorm_smul line 16
theorem OAI.RegularPointCoordinates.harmonicAffineResidualNorm_smul line 24
theorem OAI.RegularPointCoordinates.restrictLp_eq_zero_of_harmonicTargetNorm_eq_zero line 35
Source documentation
Full support makes the averaging factor nonzero on every positive ball.
```
theorem restrictLp_eq_zero_of_harmonicTargetNorm_eq_zero (p : X) {r : ℝ} (hr : 0 < r)
    (w : SobolevSpace (hausdorff n X) hX.quadratic)
    (hw : harmonicTargetNorm hX p r w = 0) :
    SobolevSpace.restrictLp (hausdorff n X) hX.quadratic (ball p r) w = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.harmonicTargetNorm, OAI.RegularPointCoordinates.SobolevSpace.restrictLp
theorem OAI.RegularPointCoordinates.harmonicAffineResidualNorm_eq_zero_on_smaller line 50
Source documentation
A zero target on the outer ball has zero affine residual on any inner ball.
```
theorem harmonicAffineResidualNorm_eq_zero_on_smaller
    (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic) (p : X) {r t : ℝ}
    (hr : 0 < r) (htr : t ≤ r) (w : SobolevSpace (hausdorff n X) hX.quadratic)
    (hw : harmonicTargetNorm hX p r w = 0) :
    harmonicAffineResidualNorm hX u p t w = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.harmonicTargetNorm, OAI.RegularPointCoordinates.harmonicAffineResidualNorm
theorem OAI.RegularPointCoordinates.HasNormalizedAffineImprovement.homogeneous line 64
Source documentation
The unit-norm estimate implies the full homogeneous estimate, including the zero-norm case.
```
theorem HasNormalizedAffineImprovement.homogeneous
    {u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic} {p : X} {r θ : ℝ}
    (hfit : HasNormalizedAffineImprovement hX u p r θ) (hr : 0 < r) (hθ : θ ≤ 1)
    (w : SobolevSpace (hausdorff n X) hX.quadratic)
    (hw : IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p r) w) :
    harmonicAffineResidualNorm hX u p (θ * r) w ≤
      (1 / 2 : ℝ) * θ * Real.sqrt θ * harmonicTargetNorm hX p r w := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.HasNormalizedAffineImprovement, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.harmonicAffineResidualNorm, OAI.RegularPointCoordinates.harmonicTargetNorm