BoundedSourceIntegral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating the bounded curvature and endpoint source estimates

theorem OAI.RegularPointCoordinates.exists_short_bounded_source_integral_bound line 23

Source documentation

The complete short-time bounded-source contribution has the square of the averaging radius.

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

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds

theorem OAI.RegularPointCoordinates.exists_long_bounded_source_integral_bound line 53

Source documentation

All long-time bounded-source blocks sum to r times the working radius. This is the gain needed for the curvature contribution.

theorem exists_long_bounded_source_integral_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 : ℕ) (x q : X),
      μ (ball q (R / 2 ^ i)) ≠ ∞ → 0 < μ.real (ball q (R / 2 ^ i)) →
      dist x q ≤ A * (R / 2 ^ i) →
      (∀ j, μ.real (ball x (R / 2 ^ j)) ≤ W * (R / 2 ^ j) ^ n) →
      (∀ t, 0 < t → t ≤ R ^ 2 → ∀ z ∈ ball x R,
        V * (Real.sqrt t) ^ n ≤ μ.real (ball z (Real.sqrt t))) →
      ∀ (f : Lp ℝ 2 μ) (B : ℝ), 0 ≤ B → (∀ᵐ z ∂μ, |f z| ≤ B) →
      (∀ᵐ z ∂μ, z ∉ ball x R → f z = 0) →
      |∫ t in (R / 2 ^ i) ^ 2..R ^ 2,
…

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