AffineFamily.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.LocalDistanceConverges.of_pointwise line 23
theorem OAI.AffineBernstein.LocalDistanceConverges.homeomorph line 56
theorem OAI.AffineBernstein.LocalDistanceConverges.diagonal line 100
structure OAI.AffineBernstein.InAffineLimitFamily line 129
Source comment
Literal full-dimensional affine local-limit family of geometry.tex:87. The affine maps may vary along the approximating sequence.
```
structure InAffineLimitFamily {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    (D : Set E) (C : Set F) : Prop where
…
```
theorem OAI.AffineBernstein.InAffineLimitFamily.nonempty line 142
theorem OAI.AffineBernstein.InAffineLimitFamily.affine_image line 146
theorem OAI.AffineBernstein.InAffineLimitFamily.diagonal_closure line 169
theorem OAI.AffineBernstein.InAffineLimitFamily.of_affine_image line 178

theorem OAI.AffineBernstein.matrixLinearEquiv_apply line 194

Source comment

The coordinate action of the actual matrix linear equivalence.

theorem matrixLinearEquiv_apply {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ)
    (hA : IsUnit A.det) (x : Space n) (i : Fin n) :
    Matrix.toLinearEquiv (EuclideanSpace.basisFun (Fin n) ℝ).toBasis A hA x i =
      A.mulVec x i := by
…

Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.convex_sum_mem_le_one line 204

Source comment

A convex combination allowing unused mass at the origin.

theorem convex_sum_mem_le_one {E : Type*} [AddCommGroup E] [Module ℝ E]
    {ι : Type*} [Fintype ι] {K : Set E} (hK : Convex ℝ K) (h0 : (0 : E) ∈ K)
    (c : ι → ℝ) (v : ι → E) (hc : ∀ i, 0 ≤ c i)
    (hsum : ∑ i, c i ≤ 1) (hv : ∀ i, v i ∈ K) : (∑ i, c i • v i) ∈ K := by
…

theorem OAI.AffineBernstein.symmetric_convex_sum_mem line 222

Source comment

The cross-polytope spanned by any points of a symmetric convex body lies in that body. This is the inner-inclusion half of max-determinant normalization.

theorem symmetric_convex_sum_mem {n : ℕ} {K : Set (Space n)}
    (hK : Convex ℝ K) (h0 : (0 : Space n) ∈ K)
    (hneg : ∀ x ∈ K, -x ∈ K) (v : Fin n → Space n)
    (hv : ∀ i, v i ∈ K) (c : Fin n → ℝ) (hc : ∑ i, |c i| ≤ 1) :
    (∑ i, c i • v i) ∈ K := by
…

Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.sum_abs_coordinate_le line 239
Source comment
The exact ℓ¹/Euclidean comparison used for the inner ball.
```
theorem sum_abs_coordinate_le {n : ℕ} (x : Space n) :
    ∑ i, |x i| ≤ Real.sqrt n * ‖x‖ := by
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.norm_le_sqrt_card_of_coordinate_le line 249
Source comment
The exact ℓ∞/Euclidean comparison used for the outer ball.
```
theorem norm_le_sqrt_card_of_coordinate_le {n : ℕ} (x : Space n)
    (hx : ∀ i, |x i| ≤ 1) : ‖x‖ ≤ Real.sqrt n := by
…
```
Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.exists_max_det_columns line 265

Source comment

A compact body's column determinant has a maximizer, with nonzero value whenever the body contains a ball about zero.

theorem exists_max_det_columns {n : ℕ} {K : Set (Space n)}
    (hK : IsCompact K) {r : ℝ} (hr : 0 < r)
    (hball : Metric.closedBall (0 : Space n) r ⊆ K) :
    ∃ v : Fin n → Space n, (∀ i, v i ∈ K) ∧
      (Matrix.det (fun i j => v j i) ≠ 0) ∧
      ∀ w : Fin n → Space n, (∀ i, w i ∈ K) →
        |Matrix.det (fun i j => w j i)| ≤ |Matrix.det (fun i j => v j i)| := by
…

Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.maxdet_coordinate_bound line 297

Source comment

Maximal determinant makes each inverse coordinate of a body point at most one. The proof is the literal one-column replacement identity.

theorem maxdet_coordinate_bound {n : ℕ} {K : Set (Space n)}
    (v : Fin n → Space n) (hv : ∀ i, v i ∈ K)
    (hd : Matrix.det (fun i j => v j i) ≠ 0)
    (hmax : ∀ w : Fin n → Space n, (∀ i, w i ∈ K) →
      |Matrix.det (fun i j => w j i)| ≤ |Matrix.det (fun i j => v j i)|) :
    ∃ q : Space n ≃ₗ[ℝ] Space n,
      (∀ x : Space n, q x = ∑ i, x i • v i) ∧
      ∀ x ∈ K, ∀ i, |q.symm x i| ≤ 1 := by
…

Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.symmetric_body_normalization line 339

Source comment

The symmetric max-determinant normalization, with the exact weaker radius n sufficient for all centered normalizations used in the source.

theorem symmetric_body_normalization {n : ℕ} (hn : 1 ≤ n)
    {K : Set (Space n)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (h0 : (0 : Space n) ∈ K) (hneg : ∀ x ∈ K, -x ∈ K)
    {r : ℝ} (hr : 0 < r) (hball : Metric.closedBall (0 : Space n) r ⊆ K) :
    ∃ A : Space n ≃L[ℝ] Space n,
      Metric.closedBall 0 1 ⊆ A '' K ∧ A '' K ⊆ Metric.closedBall 0 n := by
…

Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.centered_body_normalization line 380

Source comment

Exact centered normalization in geometry.tex (2/(C+1), 2n), proved without importing John's theorem: first normalize the symmetric difference body, then use the actual balance inclusion.

theorem centered_body_normalization {n : ℕ} (hn : 1 ≤ n)
    {K : Set (Space n)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hint : (interior K).Nonempty) (h0 : (0 : Space n) ∈ K)
    {C : ℝ} (hC : 1 ≤ C) (hbal : -K ⊆ C • K) :
    ∃ A : Space n ≃L[ℝ] Space n,
      Metric.closedBall 0 (2 / (C + 1)) ⊆ A '' K ∧
      A '' K ⊆ Metric.closedBall 0 (2 * n) := by
…

Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.simplex_ball_coordinates line 451

Source comment

A dimension-only inscribed ball in the standard simplex. This allows noncentered model fibers to be normalized without importing John's theorem.

theorem simplex_ball_coordinates {n : ℕ} (hn : 1 ≤ n) (z : Space n)
    (hz : z ∈ Metric.closedBall (WithLp.toLp 2 (fun _ : Fin n => (1 : ℝ) / (n + 1)))
      (1 / ((n : ℝ) + 1) ^ 2)) :
    (∀ i, 0 ≤ z i) ∧ (∑ i, z i) ≤ 1 := by
…

Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.noncentered_body_normalization line 487

Source comment

A linear normalization of an arbitrary full-dimensional compact convex body containing the distinguished origin. The dimension-only outer radius is intentionally not John's sharp radius; it suffices for the compactness argument and does not alter the source's final centered normalization.

theorem noncentered_body_normalization {n : ℕ} (hn : 1 ≤ n)
    {K : Set (Space n)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hint : (interior K).Nonempty) (h0 : (0 : Space n) ∈ K) :
    ∃ (A : Space n ≃L[ℝ] Space n) (c : Space n),
      Metric.closedBall c 1 ⊆ A '' K ∧
      A '' K ⊆ Metric.closedBall 0 (2 * ((n : ℝ) + 1) ^ 3) ∧
      ‖c‖ ≤ 2 * ((n : ℝ) + 1) ^ 3 := by
…

Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.noncentered_body_normalization_all line 567

Source comment

The same intermediate normalization with the zero-dimensional convention made explicit. Its radii are only used in compactness arguments.

theorem noncentered_body_normalization_all {n : ℕ}
    {K : Set (Space n)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hint : (interior K).Nonempty) (h0 : (0 : Space n) ∈ K) :
    ∃ (A : Space n ≃L[ℝ] Space n) (c : Space n),
      Metric.closedBall c 1 ⊆ A '' K ∧
      A '' K ⊆ Metric.closedBall 0 (2 * ((n : ℝ) + 1) ^ 3) ∧
      ‖c‖ ≤ 2 * ((n : ℝ) + 1) ^ 3 := by
…

Mentions: OAI.AffineBernstein.Space