HeatWeightedEvaluation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Weighted point evaluations of the actual heat semigroup

The local parabolic estimate and the signed Davies weight retain the sharp quadratic cost in the exponent. No Gaussian bound is used.

theorem OAI.RegularPointCoordinates.radialWeight_ball_lower line 21
theorem OAI.RegularPointCoordinates.heatAt_ball_weighted_square_bound line 37

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_weighted_evaluation line 77

Source documentation

Weighted point evaluation, for any continuous heat representative. The positive parameter M bounds the weighted initial L² norm.

theorem heat_weighted_evaluation :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (q x : X) (a R r t M : ℝ),
      0 ≤ R → 0 < r → -1 ≤ K*r^2 → r^2 < t → 0 < M →
      ∀ (f : Lp ℝ 2 (hausdorff n X)) (v : X → ℝ), Continuous v →
      (v =ᵐ[hausdorff n X] heatAt (hausdorff n X) hX.quadratic t f) →
      (∫ y, radialWeight q a R y*(f y)^2 ∂hausdorff n X) ≤ M^2 →
      |v x| ≤ C/Real.sqrt ((hausdorff n X).real (ball x r))*
        (Real.exp ((-a*min (dist q x) R+|a| *r)/2+a^2/4*t)*M) := by
…

Mentions: OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.heatAt, OAI.RegularPointCoordinates.radialWeight