ScaledProjectionData.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Rescaling the actual affine projection and its Euler equation

def OAI.RegularPointCoordinates.radiusScaledColumns line 19
Source documentation
Coordinate rescaling uses the same Sobolev representatives.
```
def radiusScaledColumns {n : ℕ} (r : ℝ) (u : Fin n → SobolevSpace μ hQ) :
    Fin n → SobolevSpace μ hQ := fun j => r⁻¹ • u j
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.radiusScaledColumns_column line 23
theorem OAI.RegularPointCoordinates.radiusScaledColumns_affineResidual line 32
Source documentation
The physical inverse radius preserves the affine subspace and the actual orthogonal projection.
```
theorem radiusScaledColumns_affineResidual {n : ℕ} {r : ℝ} (hr : r ≠ 0)
    (u : Fin n → SobolevSpace μ hQ) (Ω : Set X) (hfin : μ Ω ≠ ∞) :
    affineResidual μ hQ (radiusScaledColumns μ hQ r u) Ω hfin =
      affineResidual μ hQ u Ω hfin := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.affineResidual, OAI.RegularPointCoordinates.radiusScaledColumns

theorem OAI.RegularPointCoordinates.radius_scaled_projection line 47

Source documentation

The same residual, divided by the squared physical radius, is the actual projection residual of the rescaled target and coordinates.

theorem radius_scaled_projection {n : ℕ} {r : ℝ} (hr : r ≠ 0)
    (u : Fin n → SobolevSpace μ hQ) (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (v w : SobolevSpace μ hQ)
    (hw : SobolevSpace.restrictLp μ hQ Ω w =
      affineResidual μ hQ u Ω hfin (SobolevSpace.restrictLp μ hQ Ω v)) :
    SobolevSpace.restrictLp μ hQ Ω ((r ^ 2)⁻¹ • w) =
      affineResidual μ hQ (radiusScaledColumns μ hQ r u) Ω hfin
        (SobolevSpace.restrictLp μ hQ Ω ((r ^ 2)⁻¹ • v)) := by
…

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

theorem OAI.RegularPointCoordinates.radius_scaled_projection_euler line 59

Source documentation

Radial rescaling and residual amplitude rescaling preserve the exact Euler equation; the coordinate coefficient is divided by one radius.

theorem radius_scaled_projection_euler {n : ℕ} {r B B' : ℝ} (hr : 0 < r)
    (Ω : Set X) (u : Fin n → SobolevSpace μ hQ)
    (f w η e : SobolevSpace μ hQ) (ell : Euclidean n) (k : ℝ)
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (hf' : ∀ᵐ x ∂μ.restrict Ω,
      localGamma μ hQ ((r ^ 2)⁻¹ • f) ((r ^ 2)⁻¹ • f) x ≤ B')
    (hid : localRadialDerivative μ hQ Ω f hf w = SobolevSpace.restrictLp μ hQ Ω
      (w + sobolevColumnMap μ hQ u ell + k • η + e)) :
    r ^ 2 • localRadialDerivative μ hQ Ω ((r ^ 2)⁻¹ • f) hf' ((r ^ 2)⁻¹ • w) =
      SobolevSpace.restrictLp μ hQ Ω
        ((r ^ 2)⁻¹ • w + sobolevColumnMap μ hQ (radiusScaledColumns μ hQ r u) (r⁻¹ • ell) +
          ((r ^ 2)⁻¹ * k) • η + (r ^ 2)⁻¹ • e) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.radiusScaledColumns