ShortAverageMass.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The short-time average of the full source has the actual dyadic envelope

theorem OAI.RegularPointCoordinates.exists_short_average_mass_bound line 26

Source documentation

The short-time local positive source is bounded uniformly on the whole interval, before time integration and polarization.

theorem exists_short_average_mass_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 →ᵇ ℝ),
      ∀ hcompact : 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 : ℝ) (ht : 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),
      (R / 2 ^ i) ^ 2 * ⟪v, cutoffAverageHeatMass μ hQ hk χ.continuous hcompact
…

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