LongAverageMassIntegral.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Integrated long-time blocks of the actual full positive source

def OAI.RegularPointCoordinates.cutoffHeatMassAt line 22
Source documentation
The actual pointwise heat mass as a function of all real times.
```
def cutoffHeatMassAt (M : PositiveBilinearMeasure X E) (t : ℝ) (x : X) : E →L[ℝ] E :=
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure
theorem OAI.RegularPointCoordinates.cutoffHeatMassAt_of_pos line 26

theorem OAI.RegularPointCoordinates.exists_long_average_mass_integral_bound line 32

Source documentation

Each complete long-time block consumes the displacement factor r/s in the same full Bochner envelope.

theorem exists_long_average_mass_integral_bound (hg : HasCoordinateHeatBounds μ ker)
    (hdiff : HasGaussianHeatDifferenceBounds μ 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 →ᵇ ℝ),
      ∀ hcompact : HasCompactSupport (χ : X → ℝ), (∀ z, 0 ≤ χ z ∧ χ z ≤ 1) →
      (∀ z ∉ ball x R, χ z = 0) → ∀ (j : ℕ) (r : ℝ) (q : X),
      0 < r → r ≤ (R / 2 ^ j) / 2 → μ (ball q r) ≠ ∞ →
      0 < μ.real (ball q r) → dist x q ≤ A * r →
      (∀ t ∈ Icc ((R / 2 ^ j) ^ 2 / 4) ((R / 2 ^ j) ^ 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.HasGaussianHeatDifferenceBounds, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean