ScalarIterationRegularity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed local elliptic operator gains two derivatives at every step of its inhomogeneous resolvent chain. The estimates stay on one open ball.

theorem OAI.PositiveEinsteinFour.Geometry.scalar_iterate_open_integer_gain line 21