ConstantLaplacianBochnerInput.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Local constant-Laplacian calculus on the required finite span

The input is the local specialization of Gigli (2018), Theorem 3.3.8, together with Han (2018), Proposition 3.2 and Theorem 3.3. Local test regularity is as in Connell et al. (2021), Lemmas 2.6--2.7. Only the span of n harmonic coordinates and two Poisson replacements is used. The scalar shifted lower bound follows by expanding |Hess f - b g|² >= 0 and using tr Hess f = Δf on the noncollapsed n-dimensional space.

def OAI.RegularPointCoordinates.IsConstantLaplacianOn line 31
Source documentation
The actual local weak equation with a constant source.
```
def IsConstantLaplacianOn (Ω : Set X) (f : SobolevSpace μ hQ) (c : ℝ) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.isConstantLaplacianOn_zero_iff line 36
theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.mono line 43
theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.add line 60
theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.smul line 69
theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.sub line 77
theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.sub_harmonic line 86
theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.linearCombination line 94
def OAI.RegularPointCoordinates.LocalConstantLaplacianBochnerInput line 117
Source documentation
local Bochner calculus, restricted to the n+2 directions used in the Poisson comparison. The volume in the trace correction is restricted to the interior ball and hence is finite.
```
def LocalConstantLaplacianBochnerInput {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD