NormalizedCoordinateFrames.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Adjoint coordinate frames from exact mean normalization

def OAI.RegularPointCoordinates.coordinateFrame line 17
Source documentation
The pointwise coordinate change associated to a coefficient frame.
```
def coordinateFrame (A : E ≃L[ℝ] E) : E ≃L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.coordinateFrame_apply line 23

theorem OAI.RegularPointCoordinates.coordinateFrame_le_of_mean_comparison line 31

Source documentation

A relative mean bound controls the adjoint coordinate frames without an absolute lower eigenvalue assumption.

theorem coordinateFrame_le_of_mean_comparison
    (s t : Set X) (hs : MeasurableSet s) (ht : MeasurableSet t)
    (A B : E ≃L[ℝ] E)
    (hA : IsExactMeanNormalization μ hQ U s hs A)
    (hB : IsExactMeanNormalization μ hQ U t ht B)
    (hcompare : ∀ v, (1 / 4 : ℝ) * ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ ≤
      ⟪v, sobolevMeanGram μ hQ U t ht v⟫_ℝ) (w : E) :
    ‖coordinateFrame B w‖ ≤ 2 * ‖coordinateFrame A w‖ := by
…

Mentions: OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.coordinateFrame

theorem OAI.RegularPointCoordinates.norm_le_coordinateFrame_of_mean_upper line 62
Source documentation
A uniform upper bound for raw mean energy gives a uniform lower bound for every exact adjoint coordinate frame.
```
theorem norm_le_coordinateFrame_of_mean_upper
    (s : Set X) (hs : MeasurableSet s) (A : E ≃L[ℝ] E)
    (hA : IsExactMeanNormalization μ hQ U s hs A)
    {C : ℝ} (hC : 0 ≤ C)
    (hupper : ∀ v, ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ ≤ C ^ 2 * ‖v‖ ^ 2)
    (w : E) : ‖w‖ ≤ C * ‖coordinateFrame A w‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.coordinateFrame