RegularizedMonotoneHeat.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A single regularization for monotone harmonic heat Grams

The regularizer is constructed from the actual annular error and the curvature term. Positivity is proved uniformly in the direction and pole; it is not assumed as an additional heat-flow input.

def OAI.RegularPointCoordinates.harmonicHeatDerivative line 30
theorem OAI.RegularPointCoordinates.harmonicHeatDerivative_bounds line 41
Source documentation
The regularized derivative lies between twice the heat mass and that mass plus a uniform scalar error.
```
theorem harmonicHeatDerivative_bounds (hρr : ρ < r) (hκ : 0 ≤ κ)
    {t : ℝ} (ht : 0 < t) (x : X) {η lambda : ℝ}
    (herr : ‖harmonicHeatError μ hQ (k := k) G χ t x‖ ≤ η)
…
```
Mentions: OAI.RegularPointCoordinates.harmonicHeatError

theorem OAI.RegularPointCoordinates.harmonicHeatQuadratic_hasDerivAt line 79

Source documentation

An actual operator derivative also differentiates every quadratic value.

theorem harmonicHeatQuadratic_hasDerivAt (hρ : 0 < ρ) (hρr : ρ < r)
    {t : ℝ} (ht : 0 < t) (x : X) {lambda : ℝ} (hlambda : 0 ≤ lambda) (v : Euclidean n) :
    HasDerivAt (fun s => ⟪v, cutoffHeatGramAt μ hQ hk χ.weight.continuous
      (χ.hasCompactSupport μ hQ) U s x lambda v⟫_ℝ)
      ⟪v, harmonicHeatDerivative μ hQ hk G χ ht x lambda v⟫_ℝ t := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.cutoffHeatGramAt, OAI.RegularPointCoordinates.harmonicHeatDerivative

theorem OAI.RegularPointCoordinates.exists_monotone_regularized_heat line 92

Source documentation

Uniform annular decay constructs one strictly positive regularizer valid for every inner pole and every direction on a common time interval.

theorem exists_monotone_regularized_heat (hg : HasCoordinateHeatBounds μ k)
    (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
    {D V η : ℝ} (hD : 0 < D) (hV : 0 < V) (hη : 0 < η)
    (hvol : ∀ y, ρ ≤ dist p y → dist p y ≤ 2 * ρ →
      ∀ s, 0 < s → s ≤ D → V * s ^ n ≤ μ.real (ball y s)) :
    ∃ δ : ℝ, 0 < δ ∧ ∃ lambda : ℝ, 0 < lambda ∧
      lambda = 2 * κ * (L : ℝ) ^ 2 + η ∧
      ∀ x ∈ ball p (ρ / 2), ∀ v : Euclidean n,
        MonotoneOn (fun t => ⟪v, cutoffHeatGramAt μ hQ hk χ.weight.continuous
          (χ.hasCompactSupport μ hQ) U t x lambda v⟫_ℝ) (Ioo 0 δ) := by
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.cutoffHeatGramAt

theorem OAI.RegularPointCoordinates.exists_antitone_regularized_inverse line 128

Source documentation

Inverting the actual positive heat Gram reverses its time order.

theorem exists_antitone_regularized_inverse (hg : HasCoordinateHeatBounds μ k)
    (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
    {D V η : ℝ} (hD : 0 < D) (hV : 0 < V) (hη : 0 < η)
    (hvol : ∀ y, ρ ≤ dist p y → dist p y ≤ 2 * ρ →
      ∀ s, 0 < s → s ≤ D → V * s ^ n ≤ μ.real (ball y s)) :
    ∃ δ : ℝ, 0 < δ ∧ ∃ lambda : ℝ, ∃ hlambda : 0 < lambda,
      lambda = 2 * κ * (L : ℝ) ^ 2 + η ∧
      ∀ x ∈ ball p (ρ / 2), ∀ s t (hs : 0 < s) (hst : s ≤ t), t < δ →
        ((cutoffHeatGramEquiv μ hQ hk χ.weight.continuous (χ.hasCompactSupport μ hQ)
            U (fun z => (χ.bounds z).1) hs x hlambda).symm.toContinuousLinearMap -
         (cutoffHeatGramEquiv μ hQ hk χ.weight.continuous (χ.hasCompactSupport μ hQ)
            U (fun z => (χ.bounds z).1) (hs.trans_le hst) x hlambda).symm.toContinuousLinearMap).IsPositive := by
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.cutoffHeatGramEquiv