NormalizationRebase.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Rebasing all exact normalizers in one working-scale frame

theorem OAI.RegularPointCoordinates.normalized_column_rebase line 20
Source documentation
Changing the original working frame does not change any of the subsequently normalized scalar functions.
```
theorem normalized_column_rebase (U : E →L[ℝ] SobolevSpace μ hQ)
    (T S : E ≃L[ℝ] E) :
    (U.comp (T : E →L[ℝ] E)).comp (S.trans T.symm : E →L[ℝ] E) =
      U.comp (S : E →L[ℝ] E) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace

theorem OAI.RegularPointCoordinates.exact_mean_normalization_rebase line 29

Source documentation

Exact mean normalization transports through a working-frame change.

theorem exact_mean_normalization_rebase (U : E →L[ℝ] SobolevSpace μ hQ)
    (T S : E ≃L[ℝ] E) (s : Set X) (hs : MeasurableSet s)
    (hS : IsExactMeanNormalization μ hQ U s hs S) :
    IsExactMeanNormalization μ hQ (U.comp (T : E →L[ℝ] E)) s hs (S.trans T.symm) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsExactMeanNormalization

theorem OAI.RegularPointCoordinates.transformedColumn_rebase line 40
Source documentation
The operation agrees componentwise with the actual transformed columns.
```
theorem transformedColumn_rebase {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (T S : Euclidean n ≃L[ℝ] Euclidean n) :
    transformedColumn μ hQ (transformedColumn μ hQ u T) (S.trans T.symm) =
      transformedColumn μ hQ u S := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.transformedColumn
theorem OAI.RegularPointCoordinates.firstOrderSplitting_rebase line 52
Source documentation
First-order splitting bounds are exactly preserved in every rebased normalizer, including the same scalar representatives.
```
theorem firstOrderSplitting_rebase {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (T S : Euclidean n ≃L[ℝ] Euclidean n) (p : X) (r ε : ℝ) (w : X → Euclidean n)
    (h : FirstOrderSplittingOn μ hQ p r ε (transformedColumn μ hQ u S) w) :
    FirstOrderSplittingOn μ hQ p r ε
      (transformedColumn μ hQ (transformedColumn μ hQ u T) (S.trans T.symm)) w := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn
theorem OAI.RegularPointCoordinates.dyadic_regularizer_le_working_radius line 62
Source documentation
The scalar regularizer has a uniform bound over the complete finite range whenever its outer dyadic radius lies inside the working radius.
```
theorem dyadic_regularizer_le_working_radius {r R lambda : ℝ} (hr : 0 ≤ r)
    (k : ℕ) (hR : (2 : ℝ) ^ k * r ≤ R) :
    |lambda * r ^ 2| * (2 : ℝ) ^ k ≤ |lambda| * R ^ 2 := by
…
```
theorem OAI.RegularPointCoordinates.dyadic_regularizer_le_geometric line 74
Source documentation
Keeping the dyadic room in the estimate makes the regularizer vanish at fine scales even when the working radius and regularizer are fixed.
```
theorem dyadic_regularizer_le_geometric {r R lambda : ℝ} (hr : 0 ≤ r)
    (k : ℕ) (hR : (2 : ℝ) ^ k * r ≤ R) :
    |lambda * r ^ 2| * (2 : ℝ) ^ k ≤
      (|lambda| * R ^ 2) * (1 / 2 : ℝ) ^ k := by
…
```