ScaledHeatBase.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Radius-independent heat-base bounds under dimensionless regularization

The regularizer is Lambda/R^2. At a fixed dyadic index its contribution is Lambda/4^J, so the base constant is fixed before choosing R.

theorem OAI.RegularPointCoordinates.scaled_regularizer_dyadic line 17

theorem OAI.RegularPointCoordinates.exists_scaled_dyadic_heat_base line 27

Source documentation

A single inverse-metric base bound works for every physical radius when the dimensionless regularizer and the starting index are fixed.

theorem exists_scaled_dyadic_heat_base (n J : ℕ) {Lambda Lbound : ℝ}
    (hLambda : 0 < Lambda) (hLbound : 0 ≤ Lbound) :
    ∃ T : ℝ, 0 < T ∧ ∀ (R : ℝ) (hR : 0 < R)
      (U : Euclidean n →L[ℝ] SobolevSpace μ hQ)
      (M : PositiveBilinearMeasure X (Euclidean n)) (κ r ρ C : ℝ) (p : X) (L : ℝ≥0)
      (_G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p r L v)
      (χ : GoodLaplacianCutoff μ hQ p ρ C),
      ρ < r → (L : ℝ) ^ 2 ≤ Lbound → ∀ x v,
      let Q := dyadicHeatGramAt μ hQ hk U χ x hR (div_pos hLambda (sq_pos_of_pos hR)) J
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.dyadicHeatGramAt