HarmonicBochnerHeatSource.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The canonical heat source as mass, curvature and cutoff error

A second compact cutoff legitimizes testing the full signed source against an arbitrary positive-time continuous kernel row. The resulting formula is the actual harmonic heat Gram equation, including singular Bochner mass.

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.integral_cutoffSource line 31

Source documentation

The explicit bounded-test decomposition of the full cutoff source.

theorem integral_cutoffSource (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ w : X →ᵇ ℝ) (c : SobolevSpace μ hQ) (q : Lp ℝ 2 μ) :
    (∫ᵛ z, w z ∂<•(G.cutoffSource μ hQ χ c q)) =
      2 * ⟪v, M.weightedOperator (w * χ) v⟫_ℝ -
      2 * κ * (∫ z, (w * χ) z * localGamma μ hQ (U v) (U v) z ∂μ) +
      ∫ z, w z * cutoffSourceDensity μ hQ G.energy c q z ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.cutoffSourceDensity

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.kernel_cutoffSource line 47

Source documentation

Full signed integration against a kernel row splits into the actual heat mass, the curvature term and the integrable cutoff error.

theorem kernel_cutoffSource (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (hχs : HasCompactSupport (χ : X → ℝ))
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (q : Lp ℝ 2 μ) (a : X) {R : ℝ} (hR : 0 < R)
    (hχR : ∀ z ∉ closedBall a R, χ z = 0)
    (hqR : ∀ᵐ z ∂μ, z ∉ closedBall a R → q z = 0)
    {t : ℝ} (ht : 0 < t) (x : X) :
    (∫ᵛ z, k t x z ∂<•(G.cutoffSource μ hQ χ c q)) =
      2 * ⟪v, cutoffHeatMass μ hQ hk χ.continuous hχs M ht x v⟫_ℝ -
      2 * κ * ⟪v, cutoffHeatGram μ hQ hk χ.continuous hχs U ht x 0 v⟫_ℝ +
      ∫ z, k t x z * cutoffSourceDensity μ hQ G.energy c q z ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.cutoffHeatMass, OAI.RegularPointCoordinates.cutoffHeatGram, OAI.RegularPointCoordinates.cutoffSourceDensity

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.heatGram_hasDerivAt_mass line 103

Source documentation

The actual heat Gram equation, now with the canonical mass term.

theorem heatGram_hasDerivAt_mass (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (hχs : HasCompactSupport (χ : X → ℝ))
    (hχΩ : tsupport (χ : X → ℝ) ⊆ ball p (2 * r))
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (q : Lp ℝ 2 μ) (hq : IsWeakLaplacian μ hQ c q)
    (a : X) {R : ℝ} (hR : 0 < R)
    (hχR : ∀ z ∉ closedBall a R, χ z = 0)
    (hqR : ∀ᵐ z ∂μ, z ∉ closedBall a R → q z = 0)
    {t : ℝ} (ht : 0 < t) (x : X) (lambda : ℝ) :
    HasDerivAt (fun s => ⟪v, cutoffHeatGramAt μ hQ hk χ.continuous hχs U s x lambda v⟫_ℝ)
      (2 * ⟪v, cutoffHeatMass μ hQ hk χ.continuous hχs M ht x v⟫_ℝ -
       2 * κ * ⟪v, cutoffHeatGram μ hQ hk χ.continuous hχs U ht x 0 v⟫_ℝ +
…

Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.cutoffHeatGramAt, OAI.RegularPointCoordinates.cutoffHeatMass, OAI.RegularPointCoordinates.cutoffHeatGram