LongBoundedSource.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Long-time displacement bound for the bounded curvature source

theorem OAI.RegularPointCoordinates.exists_long_bounded_source_bound line 21

Source documentation

On each long-time block the bounded source gains the displacement ratio r/s. The volume bound is only needed on the working ball.

theorem exists_long_bounded_source_bound (hg : HasCoordinateHeatBounds μ ker)
    (hdiff : HasGaussianHeatDifferenceBounds μ ker)
    (n : ℕ) {A V W : ℝ} (hA : 0 ≤ A) (hV : 0 < V) (hW : 0 ≤ W) :
    ∃ C : ℝ, 0 < C ∧ ∀ (R : ℝ), 0 < R → R ≤ 1 → ∀ (i : ℕ) (r : ℝ) (x q : X),
      0 < r → r ≤ (R / 2 ^ i) / 2 → μ (ball q r) ≠ ∞ → 0 < μ.real (ball q r) →
      dist x q ≤ A * r →
      (∀ j ≤ i, μ.real (ball x (2 ^ j * (R / 2 ^ i))) ≤ W * (2 ^ j * (R / 2 ^ i)) ^ n) →
      ∀ (t : ℝ), 0 < t → t ∈ Icc ((R / 2 ^ i) ^ 2 / 4) ((R / 2 ^ i) ^ 2) →
      (∀ z ∈ ball x R, V * (Real.sqrt t) ^ n ≤ μ.real (ball z (Real.sqrt t))) →
      ∀ (g : X → ℝ) (B : ℝ), 0 ≤ B → (∀ᵐ z ∂μ, |g z| ≤ B) →
      (∀ᵐ z ∂μ, z ∉ ball x R → g z = 0) →
      |∫ z, (kernelAverage μ ker t (ball q r) z - ker t x z) * g z ∂μ| ≤
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds, OAI.RegularPointCoordinates.kernelAverage