AverageMassTime.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual short-time source integrals

def OAI.RegularPointCoordinates.cutoffAverageHeatMassAt line 22
Source documentation
The actual averaged heat mass, set to zero outside positive times.
```
def cutoffAverageHeatMassAt (M : PositiveBilinearMeasure X E)
    (s : Set X) (hs : MeasurableSet s) (hbounded : Bornology.IsBounded s) (t : ℝ) : E →L[ℝ] E :=
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure
theorem OAI.RegularPointCoordinates.cutoffAverageHeatMassAt_of_pos line 26
theorem OAI.RegularPointCoordinates.cutoffAverageHeatMassAt_nonneg line 32

theorem OAI.RegularPointCoordinates.exists_short_average_mass_integral_bound line 44

Source documentation

The entire short-time source integral is bounded by the actual Bochner envelope, with the same uniform constant as the pointwise estimate.

theorem exists_short_average_mass_integral_bound (hg : HasCoordinateHeatBounds μ ker)
    (m : ℕ) {A V : ℝ} (hA : 0 ≤ A) (hV : 0 < V) :
    ∃ C : ℝ, 0 < C ∧ ∀ (M : PositiveBilinearMeasure X (Euclidean (m + 2)))
      (R : ℝ) (_hR : 0 < R), R ≤ 1 → ∀ (x : X) (χ : X →ᵇ ℝ),
      ∀ hc : HasCompactSupport (χ : X → ℝ), (∀ z, 0 ≤ χ z ∧ χ z ≤ 1) →
      (∀ z ∉ ball x R, χ z = 0) → ∀ (i : ℕ) (q : X),
      μ (ball q (R / 2 ^ i)) ≠ ∞ →
      V * (R / 2 ^ i) ^ (m + 2) ≤ μ.real (ball q (R / 2 ^ i)) →
      dist x q ≤ A * (R / 2 ^ i) →
      (∀ t, 0 < t → t ≤ (R / 2 ^ i) ^ 2 →
        ∀ z, χ z ≠ 0 → V * (Real.sqrt t) ^ (m + 2) ≤ μ.real (ball z (Real.sqrt t))) →
      ∀ v : Euclidean (m + 2),
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean