TransformationInput.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact-normalization part of the published transformation theorem

This is the pointwise-in-scale consequence of Huang--Huang (2024), Theorem 4.1(1)--(2), using the first-order criterion after Definition 2.7. The initial first-order data are on a doubled ball. The additional no-(n+1)-Euclidean condition is present explicitly, and will be supplied by the proved finite-dimensional obstruction.

theorem OAI.RegularPointCoordinates.FirstOrderSplittingOn.mono_error line 29
def OAI.RegularPointCoordinates.LocalTransformationInput line 42
Source documentation
A precisely cited conditional input. It retains both the flatness and no-extra-factor hypotheses of Theorem 4.1. Only its first two conclusions are requested here; interscale growth is not assumed as part of this input.
```
def LocalTransformationInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD