GradientProductInput.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

gradient-product bound on the same local Poisson span

Gigli (2018), Proposition 3.3.22(i), equation (3.3.33), identifies the gradient of Gamma(f,g) with Hess(f)(grad g,.) + Hess(g)(grad f,.). Theorem 3.3.8, equation (3.3.18), and Han (2018), Proposition 3.2 and Theorem 3.3, bound the shifted Hessian square by the full Bochner measure. Tensor Cauchy--Schwarz and |A+B|^2 <= 2|A|^2+2|B|^2 give the bound below. The local test-function specialization is Connell et al. (2021), Lemmas 2.6--2.7. Only the n+2-dimensional span already used by the application is retained.

def OAI.RegularPointCoordinates.LocalPoissonGradientProductInput line 28
Source documentation
The gradient-product rule and shifted Hessian bound, using the same canonical local energy measure as the same local Poisson span. Locality allows any Sobolev representative of its gradient pairing.
```
def LocalPoissonGradientProductInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD