OAI/Geometry/RCD/Heat/HeatGramComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.cutoffHeatGram_lower_mean line 23

   Source documentation

   A lower kernel bound on a set where the cutoff equals one gives a lower bound by its actual mean Gram, including the positive regularizer.

   theorem cutoffHeatGram_lower_mean (s : Set X) (hs : MeasurableSet s)
       (hχpos : ∀ y, 0 ≤ χ y) (hχone : ∀ y ∈ s, χ y = 1)
       {t : ℝ} (ht : 0 < t) (x : X) {c lambda : ℝ} (hlambda : 0 ≤ lambda)
       (hkernel : ∀ y ∈ s, c * (μ.real s)⁻¹ ≤ p t x y) (v : E) :
       c * ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ ≤
         ⟪v, cutoffHeatGram μ hQ hp hχ hsχ U ht x lambda v⟫_ℝ := by
   …

   Mentions: OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.cutoffHeatGram

2. theorem OAI.RegularPointCoordinates.cutoffHeatGram_upper_mean line 56

   Source documentation

   An upper kernel bound on the support of a cutoff bounds the heat Gram by the mean Gram on the supporting set and the exact regularizer.

   theorem cutoffHeatGram_upper_mean (s : Set X) (hs : MeasurableSet s)
       (hχle : ∀ y, χ y ≤ 1) (hχzero : ∀ y ∉ s, χ y = 0)
       {t : ℝ} (ht : 0 < t) (x : X) {C lambda : ℝ}
       (hkernel : ∀ y ∈ s, p t x y ≤ C * (μ.real s)⁻¹) (v : E) :
       ⟪v, cutoffHeatGram μ hQ hp hχ hsχ U ht x lambda v⟫_ℝ ≤
         C * ⟪v, sobolevMeanGram μ hQ U s hs v⟫_ℝ + (lambda * t) * ‖v‖ ^ 2 := by
   …

   Mentions: OAI.RegularPointCoordinates.cutoffHeatGram, OAI.RegularPointCoordinates.sobolevMeanGram