RelativeHeatMean.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Converting the relative heat comparison to quadratic-form order

theorem OAI.RegularPointCoordinates.relative_heat_mean_of_conjugated_norm line 19

Source documentation

The norm estimate in an exact mean frame is precisely the relative quadratic comparison in the original, possibly ill-conditioned coordinates.

theorem relative_heat_mean_of_conjugated_norm
    (μ : Measure X) (hQ : QuadraticCheegerEnergy μ)
    (U : E →L[ℝ] SobolevSpace μ hQ) (s : Set X) (hs : MeasurableSet s)
    (A : E ≃L[ℝ] E) (hA : IsExactMeanNormalization μ hQ U s hs A)
    (Q : E →L[ℝ] E) {η : ℝ}
    (hclose : ‖(A : E →L[ℝ] E).adjoint.comp (Q.comp (A : E →L[ℝ] E)) -
      ContinuousLinearMap.id ℝ E‖ ≤ η) (v : E) :
    (1 - η) * ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ ≤ ⟪v, Q v⟫_ℝ ∧
      ⟪v, Q v⟫_ℝ ≤ (1 + η) * ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ := by
…

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