GradientProductAction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The gradient-product identity in terms of actual Hessian actions

This is the finite Sobolev-representative form of Gigli's formula (3.3.33). The identity itself is algebraic once the three Gram representatives exist.

theorem OAI.RegularPointCoordinates.localGamma_mixed_as_hessian_actions line 21
Source documentation
The two Hessian actions recover the derivative of the mixed Gram representative, including an arbitrary scalar shift.
```
theorem localGamma_mixed_as_hessian_actions
    (f a z G Fz Az : SobolevSpace μ hQ) (b : ℝ) :
    localGamma μ hQ (G-b • a) z =ᵐ[μ] fun x =>
      (localHessianAction μ hQ f a z G Fz Az x-b*localGamma μ hQ a z x)+
        localHessianAction μ hQ a f z G Az Fz x := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.localHessianAction
theorem OAI.RegularPointCoordinates.diagonal_le_of_two_actions line 32

theorem OAI.RegularPointCoordinates.localGamma_shifted_mixed_bound line 48

Source documentation

When the shifted mixed gradient is an admissible Hessian direction, the two action bounds give its exact factor-two gradient estimate.

theorem localGamma_shifted_mixed_bound
    (f a G Fz Az : SobolevSpace μ hQ) (b : ℝ) (A B : X → ℝ)
    (hA : ∀ᵐ x ∂μ, 0≤A x) (hB : ∀ᵐ x ∂μ, 0≤B x)
    (hfirst : ∀ᵐ x ∂μ,
      (localHessianAction μ hQ f a (G-b • a) G Fz Az x-
        b*localGamma μ hQ a (G-b • a) x)^2 ≤ A x*localGamma μ hQ (G-b • a) (G-b • a) x)
    (hsecond : ∀ᵐ x ∂μ,
      (localHessianAction μ hQ a f (G-b • a) G Az Fz x)^2 ≤
        B x*localGamma μ hQ (G-b • a) (G-b • a) x) :
    ∀ᵐ x ∂μ, localGamma μ hQ (G-b • a) (G-b • a) x≤2*(A x+B x) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localHessianAction, OAI.RegularPointCoordinates.localGamma