NearbyMeanGrams.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Comparing Gram means inside a common normalized region

Averaged Gram errors on an enlarged ball restrict to nearby balls with only the volume-ratio cost. If one coordinate normalization makes both resulting means close to the identity, their original quadratic forms are close to each other. These are the comparison steps after harmonic transformation.

theorem OAI.RegularPointCoordinates.average_nonneg_le_of_subset line 23
theorem OAI.RegularPointCoordinates.meanGram_sub_id_norm_le_of_subset line 44

theorem OAI.RegularPointCoordinates.meanGrams_compare_from_common_normalization line 65

Source documentation

A common approximately orthonormal coordinate change compares the original means, including when their smallest eigenvalues are very small.

theorem meanGrams_compare_from_common_normalization
    (U : E →L[ℝ] SobolevSpace μ hQ) (A : E ≃L[ℝ] E)
    (s t : Set X) (hs : MeasurableSet s) (ht : MeasurableSet t)
    {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1)
    (hsnorm : ‖sobolevMeanGram μ hQ (U.comp (A : E →L[ℝ] E)) s hs -
      ContinuousLinearMap.id ℝ E‖ ≤ δ)
    (htnorm : ‖sobolevMeanGram μ hQ (U.comp (A : E →L[ℝ] E)) t ht -
      ContinuousLinearMap.id ℝ E‖ ≤ δ) (v : E) :
    (1 - δ) * ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ ≤
        (1 + δ) * ⟪v, sobolevMeanGram μ hQ U t ht v⟫_ℝ ∧
    (1 - δ) * ⟪v, sobolevMeanGram μ hQ U t ht v⟫_ℝ ≤
        (1 + δ) * ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.sobolevMeanGram