ScaledSeparatedSources.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Separation estimates with constants fixed before the physical radius

theorem OAI.RegularPointCoordinates.exists_scaled_separated_gaussian_bound line 15

Source documentation

Rescaling the scalar Gaussian estimate retains its exact inverse-volume power.

theorem exists_scaled_separated_gaussian_bound (n : ℕ) {c D : ℝ}
    (hc : 0 < c) (hD : 0 < D) :
    ∃ C : ℝ, 0 < C ∧ ∀ R s d : ℝ, 0 < R → 0 < s → c * R ≤ d →
      R ^ n * (s⁻¹ ^ n * Real.exp (-d ^ 2 / (D * s ^ 2))) ≤ C := by
…

theorem OAI.RegularPointCoordinates.exists_scaled_short_source_bound line 38

Source documentation

The short-time source coefficient scales as inverse volume.

theorem exists_scaled_short_source_bound (hg : HasCoordinateHeatBounds μ ker)
    (n : ℕ) {A V c : ℝ} (hA : 0 ≤ A) (hV : 0 < V) (hc : 0 < c) :
    ∃ C : ℝ, 0 < C ∧ ∀ (R r t : ℝ) (x q : X) (S : Set X) (g : X → ℝ),
      0 < R → 0 < r → r ≤ 1 → 0 < t → t ≤ r ^ 2 →
      μ (ball q r) ≠ ∞ → V * r ^ n ≤ μ.real (ball q r) → dist x q ≤ A * r →
      (∀ z ∈ S, c * R ≤ dist x z) →
      (∀ z ∈ S, V * (Real.sqrt t) ^ n ≤ μ.real (ball z (Real.sqrt t))) →
      Integrable g μ → (∀ᵐ z ∂μ, z ∉ S → g z = 0) →
      |∫ z, kernelAverage μ ker t (ball q r) z * g z ∂μ| ≤
        (C / R ^ n) * ∫ z, |g z| ∂μ := by
…

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

theorem OAI.RegularPointCoordinates.exists_scaled_long_source_bound line 71

Source documentation

The long-time source difference has one extra inverse-radius factor.

theorem exists_scaled_long_source_bound (hg : HasCoordinateHeatBounds μ ker)
    (hdiff : HasGaussianHeatDifferenceBounds μ ker)
    (n : ℕ) {A V c : ℝ} (hA : 0 ≤ A) (hV : 0 < V) (hc : 0 < c) :
    ∃ C : ℝ, 0 < C ∧ ∀ (R r t : ℝ) (x q : X) (S : Set X) (g : X → ℝ),
      0 < R → 0 < r → 0 < t → t ≤ 1 → r ^ 2 ≤ t →
      μ (ball q r) ≠ ∞ → 0 < μ.real (ball q r) → dist x q ≤ A * r →
      (∀ z ∈ S, c * R ≤ dist x z) →
      (∀ z ∈ S, V * (Real.sqrt t) ^ n ≤ μ.real (ball z (Real.sqrt t))) →
      Integrable g μ → (∀ᵐ z ∂μ, z ∉ S → g z = 0) →
      |∫ z, (kernelAverage μ ker t (ball q r) z - ker t x z) * g z ∂μ| ≤
        (C * r / R ^ (n + 1)) * ∫ z, |g z| ∂μ := by
…

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