OAI/Geometry/RCD/Heat/DyadicMeanStability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.dyadicMeanGram line 16
2. theorem OAI.RegularPointCoordinates.dyadic_mean_slow_step line 37

   Source documentation

   The actual means have the same slow one-step growth as the heat metrics.

   theorem dyadic_mean_slow_step (i : ℕ) (v : Euclidean (m + 1)) :
       ⟪v, dyadicMeanGram (hausdorff (m + 1) X) hX.quadratic u p R i v⟫_ℝ ≤
         (9 / 8 : ℝ) * ⟪v, dyadicMeanGram (hausdorff (m + 1) X) hX.quadratic u p R (i + 1) v⟫_ℝ := by
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.dyadicMeanGram, OAI.RegularPointCoordinates.hausdorff

3. theorem OAI.RegularPointCoordinates.dyadic_mean_four_le_two line 58

   Source documentation

   Moving four dyadic scales inward costs less than two. This is the enlargement used by the local Bochner cutoff estimate.

   theorem dyadic_mean_four_le_two (i : ℕ) (hi : 4 ≤ i) (v : Euclidean (m + 1)) :
       ⟪v, dyadicMeanGram (hausdorff (m + 1) X) hX.quadratic u p R (i - 4) v⟫_ℝ ≤
         2 * ⟪v, dyadicMeanGram (hausdorff (m + 1) X) hX.quadratic u p R i v⟫_ℝ := by
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.dyadicMeanGram, OAI.RegularPointCoordinates.hausdorff