FramedPointValues.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of centered point values with the normalizing frame

theorem OAI.RegularPointCoordinates.framed_covector_point_values line 19

Source documentation

Continuous representatives of the same Sobolev columns have the exact covector transformation law, including at the center of an open ball.

theorem framed_covector_point_values [μ.IsOpenPosMeasure] {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (N : Euclidean n ≃L[ℝ] Euclidean n)
    (s : Set X) (hs : IsOpen s) (V W : X → Euclidean n)
    (hV : ContinuousOn V s) (hW : ContinuousOn W s)
    (hu : ∀ j, SobolevSpace.toLp μ hQ (u j) =ᵐ[μ.restrict s] fun x => V x j)
    (hNu : ∀ j, SobolevSpace.toLp μ hQ (transformedColumn μ hQ u N j) =ᵐ[
      μ.restrict s] fun x => W x j) (b : Euclidean n) :
    EqOn (fun x => ⟪W x, N.symm b⟫_ℝ) (fun x => ⟪V x, b⟫_ℝ) s := by
…

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

theorem OAI.RegularPointCoordinates.centered_frame_covector_eq line 37
Source documentation
Centering before applying the inverse covector frame gives the same actual Sobolev function as centering the original coordinate covector.
```
theorem centered_frame_covector_eq {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (N : Euclidean n ≃L[ℝ] Euclidean n)
    (η : SobolevSpace μ hQ) (c cN b : Euclidean n)
    (hc : ⟪cN, N.symm b⟫_ℝ = ⟪c, b⟫_ℝ) :
    sobolevColumnMap μ hQ (centeredColumn μ hQ (transformedColumn μ hQ u N) cN η)
      (N.symm b) = centeredAffineSobolev μ hQ u η c b := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.centeredColumn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.centeredAffineSobolev