OAI/Geometry/RCD/Sobolev/LocalPoissonMixedShifted.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Shifted mixed Hessian bounds for three actual local Poisson functions

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_mixed_shifted_bound line 18