HeatMassTail.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Missing heat mass from a dyadic shell tail

theorem OAI.RegularPointCoordinates.setIntegral_le_bound_mul_volume line 19

Source documentation

Integrating an upper bound over a subset costs at most the volume of the larger finite-measure set.

theorem setIntegral_le_bound_mul_volume (μ : Measure X) {f : X → ℝ} {s t : Set X}
    (hsub : s ⊆ t) (ht : μ t ≠ ∞) (hi : IntegrableOn f s μ)
    {C : ℝ} (hC : 0 ≤ C) (hb : ∀ᵐ x ∂μ.restrict s, f x ≤ C) :
    (∫ x in s, f x ∂μ) ≤ C * μ.real t := by
…

theorem OAI.RegularPointCoordinates.integral_outside_dyadic_ball_le_tail line 31

Source documentation

A summable shell majorant bounds exactly the heat mass outside a ball. The prefix vanishes because its shells lie inside that ball.

theorem integral_outside_dyadic_ball_le_tail (μ : Measure X) (p : X)
    {r : ℝ} (hr : 0 < r) {f : X → ℝ} (hi : Integrable f μ)
    (hfinite : ∀ s, μ (ball p s) ≠ ∞)
    {W : ℕ → ℝ} (hW : ∀ j, 0 ≤ W j)
    (hbound : ∀ j, ∀ᵐ x ∂μ.restrict (dyadicShell p r j), f x ≤ W j)
    (hsum : Summable (fun j => W j * μ.real (ball p (2 ^ j * r)))) (N : ℕ) :
    (∫ x in (ball p (2 ^ N * r))ᶜ, f x ∂μ) ≤
      ∑' j, W (j + (N + 1)) * μ.real (ball p (2 ^ (j + (N + 1)) * r)) := by
…

Mentions: OAI.RegularPointCoordinates.dyadicShell