ModelCentering.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.IsModelShape.transverse_image line 25

Source comment

Transverse coordinate changes preserve the literal model conditions.

theorem IsModelShape.transverse_image {C : Set (Space k × Space m)}
    (hC : IsModelShape C) (A : Space m ≃L[ℝ] Space m) :
    IsModelShape (((ContinuousLinearEquiv.refl ℝ (Space k)).prodCongr A) '' C) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.IsModelShape

theorem OAI.AffineBernstein.fiber_transverse_image line 51

theorem OAI.AffineBernstein.IsModelShape.supported_split line 66

Source comment

The actual support-coordinate change gives precisely the split model to which the thin-slice construction applies.

theorem IsModelShape.supported_split {C : Set (Space k × Space m)}
    (hC : IsModelShape C) (A : Space m ≃L[ℝ] ℝ × Space d)
    (hs : ∀ p ∈ C, 0 ≤ (A p.2).1)
    (hi : (1,0) ∈ interior (A '' modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))))) :
    IsSupportedSplitModel (((ContinuousLinearEquiv.refl ℝ (Space k)).prodCongr A) '' C) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.modelFiber, OAI.AffineBernstein.IsSupportedSplitModel

def OAI.AffineBernstein.thinRescalingEquiv line 106
Source comment
The rescaling is genuinely an invertible linear image, not an abstract limit operation.
```
def thinRescalingEquiv (k d : ℕ) (ε : ℝ) (hε : ε ≠ 0)
    (A : Space d ≃L[ℝ] Space d) :
    (Space k × (ℝ × Space d)) ≃L[ℝ] (Space k × (ℝ × Space d)) :=
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.thinRescaling_eq_image line 112

theorem OAI.AffineBernstein.modelShape_reorder line 122

Source comment

Reindexing the limiting (s,r) orthant gives the manuscript's exact (k+1)-model, including the case of no remaining transverse coordinates.

theorem modelShape_reorder {C : Set (Space k × (ℝ × Space d))}
    (hc : IsClosed C) (hv : Convex ℝ C) (hi : (interior C).Nonempty)
    (ho : ∀ s : Space k, (∀ i, 0 ≤ s i) → ∀ r : ℝ, 0 ≤ r → (s,(r,0)) ∈ C)
    (hs : ∀ p ∈ C, (∀ i, 0 ≤ p.1 i) ∧ 0 ≤ p.2.1)
    (hcap : ∀ T : ℝ, 0 ≤ T → IsCompact (C ∩ {p | (∑ i,p.1 i)+p.2.1 ≤ T})) :
    IsModelShape (reorderThinEquiv k d '' C) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.reorderThinEquiv

theorem OAI.AffineBernstein.IsSupportedSplitModel.exists_next_model line 166
Source comment
A supported thin-slice model produces an actual model with one additional nonnegative direction in the original affine local-limit family. All normalizers, subsequences and limiting sets are constructed here.
```
theorem IsSupportedSplitModel.exists_next_model
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E]
    {D : Set E} (hD : IsClosed D) (hneD : D.Nonempty)
    {C : Set (Space k × (ℝ × Space d))} (hC : IsSupportedSplitModel C)
    (hf : InAffineLimitFamily D C) :
    ∃ C' : Set (Space (k+1) × Space d), IsModelShape C' ∧ InAffineLimitFamily D C' := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.IsSupportedSplitModel, OAI.AffineBernstein.InAffineLimitFamily, OAI.AffineBernstein.IsModelShape

theorem OAI.AffineBernstein.IsModelShape.exists_next_model_of_zero_boundary line 220

Source comment

Boundary zero in the fiber is incompatible with maximality of the number of model directions: the missing new model is actually produced, not assumed.

theorem IsModelShape.exists_next_model_of_zero_boundary
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E]
    {D : Set E} (hD : IsClosed D) (hneD : D.Nonempty)
    {C : Set (Space k × Space m)} (hC : IsModelShape C) (hf : InAffineLimitFamily D C)
    (hz : (0 : Space m) ∉ interior (modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))))) :
    ∃ (d : ℕ) (C' : Set (Space (k+1) × Space d)),
      m = d+1 ∧ IsModelShape C' ∧ InAffineLimitFamily D C' := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.InAffineLimitFamily, OAI.AffineBernstein.modelFiber

theorem OAI.AffineBernstein.convex_smul_set_mono line 243
Source comment
Dilation of a convex body containing zero is monotone for nonnegative radii. This includes a zero inner radius.
```
theorem convex_smul_set_mono {F : Set (Space m)} (hv : Convex ℝ F) (hz : (0 : Space m) ∈ F)
    {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb : 0 < b) : a • F ⊆ b • F := by
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.centering_image_iff line 251
Source comment
Centering is unaffected by any invertible linear transverse change.
```
theorem centering_image_iff (A : Space m ≃L[ℝ] Space m) (F : Set (Space m)) (a : ℝ) :
    -(A '' F) ⊆ a • (A '' F) ↔ -F ⊆ a • F := by
…
```
Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.uniform_centering_at_one line 274

Source comment

Uniform centering for every distinguished fiber in a maximal model family. The single maximality hypothesis rules out actual (k+1)-models; it carries no centering estimate and is discharged by choosing maximal k.

theorem uniform_centering_at_one
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E]
    {D : Set E} (hD : IsClosed D) (hneD : D.Nonempty)
    (hmax : ∀ (d : ℕ), m = d+1 → ∀ C' : Set (Space (k+1) × Space d),
      IsModelShape C' → InAffineLimitFamily D C' → False) :
    ∃ a : ℝ, 1 ≤ a ∧ ∀ C : Set (Space k × Space m),
      IsModelShape C → InAffineLimitFamily D C →
      -(modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ)))) ⊆
        a • modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.InAffineLimitFamily, OAI.AffineBernstein.modelFiber

def OAI.AffineBernstein.positiveBaseEquiv line 345
Source comment
The positive diagonal base change sending s to the all-ones base point.
```
def positiveBaseEquiv (s : Space k) (hs : ∀ i, 0 < s i) : Space k ≃L[ℝ] Space k :=
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.positiveBaseEquiv_apply line 354
theorem OAI.AffineBernstein.positiveBaseEquiv_symm_apply line 357
theorem OAI.AffineBernstein.positiveBaseEquiv_self line 360
theorem OAI.AffineBernstein.IsModelShape.positive_base_image line 367
Source comment
Positive diagonal choices of the distinguished directions preserve all model properties, in particular compactness of caps.
```
theorem IsModelShape.positive_base_image {C : Set (Space k × Space m)}
    (hC : IsModelShape C) (s : Space k) (hs : ∀ i, 0 < s i) :
    IsModelShape (((positiveBaseEquiv s hs).prodCongr (ContinuousLinearEquiv.refl ℝ (Space m))) '' C) := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.positiveBaseEquiv
theorem OAI.AffineBernstein.fiber_positive_base_image line 399

theorem OAI.AffineBernstein.uniform_centering line 417

Source comment

Geometry.tex Proposition 2.7: the centering constant is uniform over all models, positive fibers, and admissible distinguished coordinates of a maximal family. Zero-dimensional transverse fibers are included.

theorem uniform_centering
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E]
    {D : Set E} (hD : IsClosed D) (hneD : D.Nonempty)
    (hmax : ∀ (d : ℕ), m = d+1 → ∀ C' : Set (Space (k+1) × Space d),
      IsModelShape C' → InAffineLimitFamily D C' → False) :
    ∃ a : ℝ, 1 ≤ a ∧ ∀ C : Set (Space k × Space m),
      IsModelShape C → InAffineLimitFamily D C → ∀ s : Space k, (∀ i, 0 < s i) →
      -(modelFiber C s) ⊆ a • modelFiber C s := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.InAffineLimitFamily, OAI.AffineBernstein.modelFiber