ScaledCoordinates.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Invertible coordinate normalization with physical scale included

def OAI.RegularPointCoordinates.scaledCoordinateEquiv line 15
Source documentation
Include the physical inverse radius in the invertible coordinate change.
```
def scaledCoordinateEquiv {n : ℕ} (A : Euclidean n ≃L[ℝ] Euclidean n)
    (c : ℝ) (hc : c ≠ 0) : Euclidean n ≃L[ℝ] Euclidean n :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.scaledCoordinateEquiv_toCLM line 19
theorem OAI.RegularPointCoordinates.scaledCoordinateEquiv_adjoint line 26
theorem OAI.RegularPointCoordinates.centered_scaledCoordinateEquiv line 33

theorem OAI.RegularPointCoordinates.normalized_approximation_rescale_four line 44

Source documentation

The normalization at radius four times the testing radius gives the radius-two metric approximation needed for harmonic compactness.

theorem normalized_approximation_rescale_four {X : Type*} [MetricSpace X] {n : ℕ}
    {p : X} {r ε : ℝ} (hr : 0 < r) (v : X → Euclidean n)
    (A : Euclidean n ≃L[ℝ] Euclidean n)
    (happ : IsPointedApproximation p 0 (4 * r) (1 / 2) ε
      (fun x => (4 * r)⁻¹ • ((A : Euclidean n →L[ℝ] Euclidean n).adjoint (v x) -
        (A : Euclidean n →L[ℝ] Euclidean n).adjoint (v p)))) :
    IsPointedApproximation p 0 r 2 (4 * ε)
      (fun x =>
        (scaledCoordinateEquiv A r⁻¹ (inv_ne_zero hr.ne') : Euclidean n →L[ℝ] Euclidean n).adjoint (v x) -
        (scaledCoordinateEquiv A r⁻¹ (inv_ne_zero hr.ne') : Euclidean n →L[ℝ] Euclidean n).adjoint (v p)) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation, OAI.RegularPointCoordinates.scaledCoordinateEquiv