RegularCoreMixedFullBall.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A common mixed Hessian estimate on the full working ball

The direction functions require only their actual L² weak Laplacians. Diagonal estimates are transferred to one fixed Sobolev Gram family and polarized outside a common null set.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_core_mixed_hessian_full_ball line 26

Source documentation

Scalar dimensional Bochner gives the mixed Hessian estimate on any finite regular family, for the prescribed full Bochner measure.

theorem NoncollapsedRCD.regular_core_mixed_hessian_full_ball {K : ℝ} {n m : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2≤n)
    (hscalar : ScalarDimensionalBochner (hausdorff n X) hX.quadratic K n)
    {V : Set X} (u : Fin m → compactLaplacianCore (hausdorff n X) hX.quadratic V)
    (p : X) {R : ℝ} (hR : 0<R)
    (a : Euclidean m) (df : SobolevSpace (hausdorff n X) hX.quadratic)
    (qf : Lp ℝ 2 (hausdorff n X))
    (hqf : IsWeakLaplacian (hausdorff n X) hX.quadratic
      (sobolevColumnMap (hausdorff n X) hX.quadratic (fun i => (u i).val) a) qf)
    (C : ℝ≥0) (hdf : ∀ᵐ x ∂hausdorff n X, |SobolevSpace.toLp (hausdorff n X) hX.quadratic df x|≤C)
    (hsf : qf =ᵐ[(hausdorff n X).restrict (ball p R)] SobolevSpace.toLp (hausdorff n X) hX.quadratic df)
    {J : ℝ} (hJK : J≤K)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.ScalarDimensionalBochner, OAI.RegularPointCoordinates.compactLaplacianCore, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.SobolevSpace.toLp