LocalBochnerInput.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The local harmonic Bochner input

The input is the finite-span, interior-ball specialization of Gigli, Non-smooth differential geometry, Mem. AMS 251 (2018), no. 1196, §3.1, equation (3.1.10), and Theorem 3.3.8. The local test-function extension uses Connell et al. (2021), Lemmas 2.6--2.7. In particular, Gamma of a locally Lipschitz harmonic function is locally W^{1,2}, and one half of its measure Laplacian plus kappa Gamma is positive. The finite measure is obtained by restricting inside the larger ball; the bounded global Sobolev representative is a cutoff extension.

This input asserts local calculus only. It does not include any mass estimate, heat estimate, pinching, coordinate approximation or chart.

def OAI.RegularPointCoordinates.harmonicBochnerSource line 34
Source documentation
The exact local measure Laplacian of the harmonic energy density.
```
def harmonicBochnerSource (U : E →L[ℝ] SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X E) (κ : ℝ) (v : E) : SignedMeasure X :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure
structure OAI.RegularPointCoordinates.LocalHarmonicEnergy line 41
Source documentation
The bounded representative and local measure equation furnished by local harmonic test calculus on an interior ball.
```
structure LocalHarmonicEnergy (U : E →L[ℝ] SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X E) (κ : ℝ) (p : X) (r : ℝ)
    (L : ℝ≥0) (v : E) where
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure
def OAI.RegularPointCoordinates.LocalHarmonicBochnerInput line 53
Source documentation
Local calculus on interior balls with eightfold room for regularity.
```
def LocalHarmonicBochnerInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD