OAI/Geometry/RCD/Heat/DyadicTimeIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.dyadic_time_integral_eq_sum line 17

   Source documentation

   Consecutive dyadic time blocks telescope exactly. Integrability is explicit, so no use is made of the undefined-integral zero convention.

   theorem dyadic_time_integral_eq_sum (f : ℝ → ℝ) {R : ℝ} (hR : 0 < R) (i : ℕ)
       (hf : IntervalIntegrable f volume ((R / (2 : ℝ) ^ i) ^ 2) (R ^ 2)) :
       (∫ t in (R / (2 : ℝ) ^ i) ^ 2..R ^ 2, f t) =
         ∑ j ∈ Finset.range i, ∫ t in (R / (2 : ℝ) ^ j) ^ 2 / 4..(R / (2 : ℝ) ^ j) ^ 2, f t := by
   …

2. theorem OAI.RegularPointCoordinates.dyadic_time_integral_abs_le line 43

   Source documentation

   A bound on each actual block gives the corresponding finite weighted sum on the entire long-time interval.

   theorem dyadic_time_integral_abs_le (f : ℝ → ℝ) {R : ℝ} (hR : 0 < R) (i : ℕ)
       (hf : IntervalIntegrable f volume ((R / (2 : ℝ) ^ i) ^ 2) (R ^ 2))
       (B : ℕ → ℝ) (hb : ∀ j < i,
         |∫ t in (R / (2 : ℝ) ^ j) ^ 2 / 4..(R / (2 : ℝ) ^ j) ^ 2, f t| ≤ B j) :
       |∫ t in (R / (2 : ℝ) ^ i) ^ 2..R ^ 2, f t| ≤ ∑ j ∈ Finset.range i, B j := by
   …