CommonFrameRadialFits.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Transporting the actual radial fits to a common frame and region

theorem OAI.RegularPointCoordinates.common_frame_radial_residual line 21

Source documentation

The common-frame residual is exactly the original residual at the transported covector, including its recentering constant.

theorem common_frame_radial_residual {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (η : SobolevSpace μ hQ)
    (G : Euclidean n →L[ℝ] SobolevSpace μ hQ) (x z : Euclidean n)
    (N M : Euclidean n ≃L[ℝ] Euclidean n) (C : Euclidean n →L[ℝ] Euclidean n)
    (b : Euclidean n) :
    G (M.symm (N b)) -
      (centeredSobolevMap μ hQ u η z).comp N.toContinuousLinearMap
        (rebasedRadialOperator N M C b) -
      ⟪z - x, C (M.symm (N b))⟫_ℝ • η =
    G (M.symm (N b)) - centeredAffineSobolev μ hQ u η x (C (M.symm (N b))) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.centeredSobolevMap, OAI.RegularPointCoordinates.rebasedRadialOperator, OAI.RegularPointCoordinates.centeredAffineSobolev

theorem OAI.RegularPointCoordinates.common_frame_radial_bounds line 37

Source documentation

The volume ratio and frame operator norm account for all losses when the original all-covector radial fit is used on the common commutator region.

theorem common_frame_radial_bounds {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (η : SobolevSpace μ hQ)
    (G : Euclidean n →L[ℝ] SobolevSpace μ hQ) (x z : Euclidean n)
    (N M : Euclidean n ≃L[ℝ] Euclidean n) (C : Euclidean n →L[ℝ] Euclidean n)
    {Ωv Ωe Ω : Set X} (hΩv : Ω ⊆ Ωv) (hΩe : Ω ⊆ Ωe)
    (hvfin : μ Ωv ≠ ∞) (hfin : μ Ω ≠ ∞)
    (hvpos : 0 < μ.real Ωv) (hepos : 0 < μ.real Ωe) (hpos : 0 < μ.real Ω)
    {V W E D : ℝ} (hE : 0 ≤ E) (hD : 0 ≤ D)
    (hvolv : μ.real Ωv ≤ V * μ.real Ω) (hvole : μ.real Ωe ≤ W * μ.real Ω)
    (hvalue : ∀ a, ‖normalizeLocalL2 μ Ωv hvfin (SobolevSpace.restrictLp μ hQ Ωv
      (G a - centeredAffineSobolev μ hQ u η x (C a)))‖ ^ 2 ≤ E * ‖a‖ ^ 2)
    (henergy : ∀ a, (μ.real Ωe)⁻¹ * (∫ t in Ωe, localGamma μ hQ
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.centeredAffineSobolev, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.centered_sobolev_constant_difference line 84
Source documentation
Centering the common harmonic column changes each covector by a locally constant function, represented by the same compact cutoff.
```
theorem centered_sobolev_constant_difference {n : ℕ}
    (Ω : Set X) (u : Fin n → SobolevSpace μ hQ) (η : SobolevSpace μ hQ)
    (z b : Euclidean n)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ)) :
    SobolevSpace.toLp μ hQ (centeredSobolevMap μ hQ u η z b - sobolevColumnMap μ hQ u b)
      =ᵐ[μ.restrict Ω] fun _ => -⟪z, b⟫_ℝ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.centeredSobolevMap, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.common_frame_radial_representative line 105

Source documentation

The transported radial family remains a representative of the derivative of the same centered coordinate map in the common frame.

theorem common_frame_radial_representative {n : ℕ}
    (Ω : Set X) (f : SobolevSpace μ hQ) (u : Fin n → SobolevSpace μ hQ)
    (η : SobolevSpace μ hQ) (z : Euclidean n)
    (N M : Euclidean n ≃L[ℝ] Euclidean n)
    (G : Euclidean n →L[ℝ] SobolevSpace μ hQ)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (hG : ∀ a, SobolevSpace.toLp μ hQ (G a) =ᵐ[μ.restrict Ω]
      localGamma μ hQ f (sobolevColumnMap μ hQ u (M a))) (b : Euclidean n) :
    SobolevSpace.toLp μ hQ (G (M.symm (N b))) =ᵐ[μ.restrict Ω]
      localGamma μ hQ f ((centeredSobolevMap μ hQ u η z).comp N.toContinuousLinearMap b) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.centeredSobolevMap