OAI/Geometry/RCD/Coordinates/RadialFitCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Canonical local radial fits and their change of coordinates

  1. def OAI.RegularPointCoordinates.radialPairingLp line 18

    Source documentation

    The actual radial pairing, as an element of the local L2 space.

    def radialPairingLp (s : Set X) (q a : SobolevSpace μ hQ) {B : ℝ}
    (ha : ∀ᵐ x ∂μ.restrict s, localGamma μ hQ a a x ≤ B) : Lp ℝ 2 (μ.restrict s) :=
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma

  2. theorem OAI.RegularPointCoordinates.radialPairingLp_representative line 22
  3. theorem OAI.RegularPointCoordinates.radialPairingLp_congr line 29

    Source documentation

    Locality identifies the L2 targets even when their cutoffs and their bounds were chosen at different scales.

    theorem radialPairingLp_congr (s : Set X) (q a q' a' : SobolevSpace μ hQ) {B B' : ℝ}
    (ha : ∀ᵐ x ∂μ.restrict s, localGamma μ hQ a a x ≤ B)
    (ha' : ∀ᵐ x ∂μ.restrict s, localGamma μ hQ a' a' x ≤ B')
    (h : localGamma μ hQ q a =ᵐ[μ.restrict s] localGamma μ hQ q' a') :
    radialPairingLp μ hQ s q a ha = radialPairingLp μ hQ s q' a' ha' := by
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.radialPairingLp

  4. theorem OAI.RegularPointCoordinates.radialPairingLp_restrict line 39

    Source documentation

    Restriction agrees with construction on the smaller testing region.

    theorem radialPairingLp_restrict {s t : Set X} (hst : t ⊆ s)
    (q a : SobolevSpace μ hQ) {B B' : ℝ}
    (ha : ∀ᵐ x ∂μ.restrict s, localGamma μ hQ a a x ≤ B)
    (ha' : ∀ᵐ x ∂μ.restrict t, localGamma μ hQ a a x ≤ B') :
    localL2Restriction μ s t hst (radialPairingLp μ hQ s q a ha) =
      radialPairingLp μ hQ t q a ha' := by
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.localL2Restriction, OAI.RegularPointCoordinates.radialPairingLp

  5. theorem OAI.RegularPointCoordinates.affineResidual_transformed line 53

    Source documentation

    Every invertible normalizing frame gives the SAME least-squares residual.

    theorem affineResidual_transformed {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (s : Set X) (hfin : μ s ≠ ∞) (A : Euclidean n ≃L[ℝ] Euclidean n) :
    affineResidual μ hQ (transformedColumn μ hQ u A) s hfin =
      affineResidual μ hQ u s hfin := by
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.affineResidual, OAI.RegularPointCoordinates.transformedColumn

  6. theorem OAI.RegularPointCoordinates.radialPairingLp_frame line 65

    Source documentation

    Applying the inverse normalizing frame to a covector recovers its original raw radial pairing in the local L2 space.

    theorem radialPairingLp_frame {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (s : Set X) (q : SobolevSpace μ hQ) (A : Euclidean n ≃L[ℝ] Euclidean n)
    (b : Euclidean n) {B B' : ℝ}
    (ha : ∀ᵐ x ∂μ.restrict s,
      localGamma μ hQ (sobolevColumnMap μ hQ (transformedColumn μ hQ u A) (A.symm b))
        (sobolevColumnMap μ hQ (transformedColumn μ hQ u A) (A.symm b)) x ≤ B)
    (ha' : ∀ᵐ x ∂μ.restrict s,
      localGamma μ hQ (sobolevColumnMap μ hQ u b) (sobolevColumnMap μ hQ u b) x ≤ B') :
    radialPairingLp μ hQ s q (sobolevColumnMap μ hQ (transformedColumn μ hQ u A) (A.symm b)) ha =
      radialPairingLp μ hQ s q (sobolevColumnMap μ hQ u b) ha' := by
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.radialPairingLp

  7. def OAI.RegularPointCoordinates.radialFitError line 82

    Source documentation

    The dimensionless least-squares error of the actual radial derivative.

    def radialFitError {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (p : X) (r : ℝ) (hfin : μ (Metric.ball p r) ≠ ∞)
    (q a : SobolevSpace μ hQ) {B : ℝ}
    (ha : ∀ᵐ x ∂μ.restrict (Metric.ball p r), localGamma μ hQ a a x ≤ B) : ℝ :=
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma

  8. theorem OAI.RegularPointCoordinates.radialFitError_nonneg line 90
  9. theorem OAI.RegularPointCoordinates.radialFitError_congr line 98

    Source documentation

    Cutoff changes preserve the dimensionless fit whenever locality identifies their actual radial derivatives on the testing ball.

    theorem radialFitError_congr {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (p : X) (r : ℝ) (hfin : μ (Metric.ball p r) ≠ ∞)
    (q a q' a' : SobolevSpace μ hQ) {B B' : ℝ}
    (ha : ∀ᵐ x ∂μ.restrict (Metric.ball p r), localGamma μ hQ a a x ≤ B)
    (ha' : ∀ᵐ x ∂μ.restrict (Metric.ball p r), localGamma μ hQ a' a' x ≤ B')
    (h : localGamma μ hQ q a =ᵐ[μ.restrict (Metric.ball p r)] localGamma μ hQ q' a') :
    radialFitError μ hQ u p r hfin q a ha = radialFitError μ hQ u p r hfin q' a' ha' := by
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.radialFitError

  10. theorem OAI.RegularPointCoordinates.radialFitError_radius_eq line 108
  11. theorem OAI.RegularPointCoordinates.radialFitError_frame line 120

    Source documentation

    The same numerical fit is obtained in every invertible normalizing frame.

    theorem radialFitError_frame {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (p : X) (r : ℝ) (hfin : μ (Metric.ball p r) ≠ ∞)
    (q : SobolevSpace μ hQ) (A : Euclidean n ≃L[ℝ] Euclidean n) (b : Euclidean n) {B B' : ℝ}
    (ha : ∀ᵐ x ∂μ.restrict (Metric.ball p r),
      localGamma μ hQ (sobolevColumnMap μ hQ (transformedColumn μ hQ u A) (A.symm b))
        (sobolevColumnMap μ hQ (transformedColumn μ hQ u A) (A.symm b)) x ≤ B)
    (ha' : ∀ᵐ x ∂μ.restrict (Metric.ball p r),
      localGamma μ hQ (sobolevColumnMap μ hQ u b) (sobolevColumnMap μ hQ u b) x ≤ B') :
    radialFitError μ hQ (transformedColumn μ hQ u A) p r hfin q
      (sobolevColumnMap μ hQ (transformedColumn μ hQ u A) (A.symm b)) ha =
    radialFitError μ hQ u p r hfin q (sobolevColumnMap μ hQ u b) ha' := by
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.radialFitError

  12. theorem OAI.RegularPointCoordinates.HasNormalizedAffineImprovement.transformed line 138

    Source documentation

    Harmonic affine improvement is a property of the affine span, so the same improvement applies after every invertible normalization.

    theorem HasNormalizedAffineImprovement.transformed {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X)
    {u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic} {p : X} {r θ : ℝ}
    (hfit : HasNormalizedAffineImprovement hX u p r θ)
    (A : Euclidean n ≃L[ℝ] Euclidean n) :
    HasNormalizedAffineImprovement hX (transformedColumn (hausdorff n X) hX.quadratic u A) p r θ := by
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.HasNormalizedAffineImprovement, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.transformedColumn