PublishedInputDischarge.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local analytic estimates for regular-point coordinates

Hausdorff measure is regular by local finiteness on proper separable spaces. Finite-span Poisson Hessian estimates imply the harmonic Bochner calculus. Heat resolvents construct cutoffs, and bounded-compression transport yields local Poincare and zero-boundary Sobolev inequalities. These estimates give harmonic mean-value bounds and Poisson gradient estimates at every radius. The heat semigroup has a continuous kernel with Gaussian bounds. Compact-test integration by parts and radial mean kernels give Euclidean harmonic Hessian estimates. Sharp annular contraction yields model Bishop--Gromov comparison, and compressed radial transport yields the squared-distance Laplacian estimate.

theorem OAI.RegularPointCoordinates.regular_coordinates_of_published_inputs line 48
Source documentation
The chart conclusion follows from local analytic estimates and pointed rescaling compactness. Finite nets and completed distance matrices give the latter; volume comparison and completeness give properness.
```
theorem regular_coordinates_of_published_inputs {K : ℝ} {n : ℕ}
    (hn : 2 ≤ n)
    (hX : NoncollapsedRCD K n X) :
    let _ := hX.properSpace hn
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD