OAI/Geometry/RCD/Metric/EuclideanSubquadraticRigidity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Entire harmonic functions with subquadratic growth are affine

Only an exhausting sequence of positive radii and positive bounds is needed. This is the Euclidean rigidity step in the transformation blow-up.

  1. theorem OAI.RegularPointCoordinates.euclidean_harmonic_affine_of_subquadratic_bounds line 16