AffineTies.lean`

43 declarations, 0 contain sorry, 0 declared as axioms

+# Generic lines avoid affine subspaces of codimension at least two

This is the general-position step used in the cell-connectivity argument. It does not assert that a nonempty cell intersection has positive surface measure.

theorem OAI.Problem358.haar_inner_level_null line 15

Source documentation

A level set of a nonzero linear functional given by an inner product is null.

theorem haar_inner_level_null {V : Type*} [NormedAddCommGroup V]
    [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
    [MeasurableSpace V] [BorelSpace V]
    (μ : Measure V) [IsAddHaarMeasure μ] {v : V} (hv : v ≠ 0) (c : ℝ) :
    μ {x : V | ⟪v, x⟫_ℝ = c} = 0 := by
…

theorem OAI.Problem358.haar_affine_tie_null line 35

Source documentation

Distinct affine slopes can agree only on a Haar-null hyperplane.

theorem haar_affine_tie_null {V : Type*} [NormedAddCommGroup V]
    [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
    [MeasurableSpace V] [BorelSpace V]
    (μ : Measure V) [IsAddHaarMeasure μ] {v w : V} (hvw : v ≠ w)
    (a b : ℝ) : μ {x : V | ⟪x, v⟫_ℝ + a = ⟪x, w⟫_ℝ + b} = 0 := by
…

theorem OAI.Problem358.ae_affine_tie_implies_slopes_eq line 48

Source documentation

In a countable affine family, equality of values almost everywhere forces equality of slopes.

theorem ae_affine_tie_implies_slopes_eq {V : Type*} [NormedAddCommGroup V]
    [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
    [MeasurableSpace V] [BorelSpace V]
    (μ : Measure V) [IsAddHaarMeasure μ] {ι : Type*} [Countable ι]
    (y : ι → V) (c : ι → ℝ) :
    ∀ᵐ x ∂μ, ∀ i j, ⟪x, y i⟫_ℝ + c i = ⟪x, y j⟫_ℝ + c j → y i = y j := by
…

theorem OAI.Problem358.ae_unique_maximizing_slope line 67

Source documentation

The finite-affine maximum has a unique maximizing slope off a null set, even if the presentation has repeated slopes.

theorem ae_unique_maximizing_slope {V : Type*} [NormedAddCommGroup V]
    [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
    [MeasurableSpace V] [BorelSpace V]
    (μ : Measure V) [IsAddHaarMeasure μ] {ι : Type*} [Fintype ι] [Nonempty ι]
    (y : ι → V) (c : ι → ℝ) :
    ∀ᵐ x ∂μ, ∃ i, (∀ j, ⟪x, y j⟫_ℝ + c j ≤ ⟪x, y i⟫_ℝ + c i) ∧
      ∀ j, ⟪x, y i⟫_ℝ + c i ≤ ⟪x, y j⟫_ℝ + c j → y j = y i := by
…

theorem OAI.Problem358.uniform_ae_affine_tie_implies_slopes_eq line 84

Source documentation

Uniform restrictions preserve the nullity of affine ties; no volume assumptions on the source set are needed for this fact.

theorem uniform_ae_affine_tie_implies_slopes_eq {d : ℕ} (K : Set (E d))
    {ι : Type*} [Countable ι] (y : ι → E d) (c : ι → ℝ) :
    ∀ᵐ x ∂uniformMeasure K, ∀ i j,
      ⟪x, y i⟫_ℝ + c i = ⟪x, y j⟫_ℝ + c j → y i = y j := by
…

theorem OAI.Problem358.uniform_ae_unique_maximizing_slope line 93

Source documentation

A finite affine maximum has an almost-everywhere unique slope under the source measure.

theorem uniform_ae_unique_maximizing_slope {d : ℕ} (K : Set (E d))
    {ι : Type*} [Fintype ι] [Nonempty ι] (y : ι → E d) (c : ι → ℝ) :
    ∀ᵐ x ∂uniformMeasure K, ∃ i,
      (∀ j, ⟪x, y j⟫_ℝ + c j ≤ ⟪x, y i⟫_ℝ + c i) ∧
      ∀ j, ⟪x, y i⟫_ℝ + c i ≤ ⟪x, y j⟫_ℝ + c j → y j = y i := by
…

theorem OAI.Problem358.GenericSegmentAvoidance.affineSpan_insert_ne_top line 124

Source documentation

Adjoining one point to a subspace of codimension at least two leaves a proper affine subspace.

theorem affineSpan_insert_ne_top (S : AffineSubspace ℝ E) (p : E)
    (hcodim : Module.finrank ℝ S.direction + 1 < Module.finrank ℝ E) :
    affineSpan ℝ (insert p (S : Set E)) ≠ ⊤ := by
…

theorem OAI.Problem358.GenericSegmentAvoidance.lineMap_not_mem_of_not_mem_affineSpan_insert line 134
Source documentation
A point outside the affine span of p and S determines a line through p which misses S, provided p itself is outside S.
```
theorem lineMap_not_mem_of_not_mem_affineSpan_insert
    (S : AffineSubspace ℝ E) {p q : E} (hp : p ∉ S)
    (hq : q ∉ affineSpan ℝ (insert p (S : Set E))) (t : ℝ) :
    AffineMap.lineMap p q t ∉ S := by
…
```

theorem OAI.Problem358.GenericSegmentAvoidance.exists_line_avoiding line 155

Source documentation

Affine subspaces of codimension at least two can be avoided by a generic line through a fixed point. The second endpoint can be chosen in any prescribed nonempty open set and outside any countable collection of proper affine subspaces.

theorem exists_line_avoiding
    {ι κ : Type*} [Countable ι] [Countable κ]
    (μ : Measure E) [IsAddHaarMeasure μ]
    (S : ι → AffineSubspace ℝ E) (H : κ → AffineSubspace ℝ E)
    (hS : ∀ i, Module.finrank ℝ (S i).direction + 1 < Module.finrank ℝ E)
    (hH : ∀ j, H j ≠ ⊤) {p : E} (hp : ∀ i, p ∉ S i)
    {U : Set E} (hU : IsOpen U) (hne : U.Nonempty) :
    ∃ q ∈ U, (∀ j, q ∉ H j) ∧
      ∀ i (t : ℝ), AffineMap.lineMap p q t ∉ S i := by
…

theorem OAI.Problem358.GenericSegmentAvoidance.exists_segment_avoiding line 180

Source documentation

Segment formulation of the general-position lemma.

theorem exists_segment_avoiding
    {ι κ : Type*} [Countable ι] [Countable κ]
    (μ : Measure E) [IsAddHaarMeasure μ]
    (S : ι → AffineSubspace ℝ E) (H : κ → AffineSubspace ℝ E)
    (hS : ∀ i, Module.finrank ℝ (S i).direction + 1 < Module.finrank ℝ E)
    (hH : ∀ j, H j ≠ ⊤) {p : E} (hp : ∀ i, p ∉ S i)
    {U : Set E} (hU : IsOpen U) (hne : U.Nonempty) :
    ∃ q ∈ U, (∀ j, q ∉ H j) ∧
      ∀ i, Disjoint (segment ℝ p q) (S i : Set E) := by
…

theorem OAI.Problem358.GenericSegmentAvoidance.finrank_direction_add_card_le_of_inner_eq line 203

Source documentation

Independent affine equations give the expected lower bound on codimension, including when the common level set is empty.

theorem finrank_direction_add_card_le_of_inner_eq
    {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    [FiniteDimensional ℝ V] {ι : Type*} [Fintype ι]
    (S : AffineSubspace ℝ V) (v : ι → V) (a : ι → ℝ)
    (hv : LinearIndependent ℝ v)
    (hS : ∀ x ∈ S, ∀ i, ⟪x, v i⟫ = a i) :
    Module.finrank ℝ S.direction + Fintype.card ι ≤ Module.finrank ℝ V := by
…

theorem OAI.Problem358.TripleCell.no_proportional_differences line 242

Source documentation

Three functions, each strictly largest somewhere, cannot have proportional differences.

theorem no_proportional_differences {X : Type*} {f g h : X → ℝ}
    (hf : ∃ x, g x < f x ∧ h x < f x)
    (hg : ∃ x, f x < g x ∧ h x < g x)
    (hh : ∃ x, f x < h x ∧ g x < h x) :
    ¬ ∃ r : ℝ, ∀ x, f x - h x = r * (f x - g x) := by
…

def OAI.Problem358.TripleCell.score line 269
Source documentation
The affine score whose slope is y and whose intercept is c.
```
def score (y : V) (c : ℝ) (x : V) : ℝ := ⟪x, y⟫ + c
```

theorem OAI.Problem358.TripleCell.no_proportional_slopes_of_tie line 273

Source documentation

At a common tie point, strict activity of all three branches excludes proportional slope differences.

theorem no_proportional_slopes_of_tie {y0 y1 y2 z : V} {c0 c1 c2 : ℝ}
    (hf : ∃ x, score y1 c1 x < score y0 c0 x ∧ score y2 c2 x < score y0 c0 x)
    (hg : ∃ x, score y0 c0 x < score y1 c1 x ∧ score y2 c2 x < score y1 c1 x)
    (hh : ∃ x, score y0 c0 x < score y2 c2 x ∧ score y1 c1 x < score y2 c2 x)
    (h01 : score y0 c0 z = score y1 c1 z)
    (h02 : score y0 c0 z = score y2 c2 z) :
    ∀ r : ℝ, r • (y0 - y1) ≠ y0 - y2 := by
…

Mentions: OAI.Problem358.TripleCell.score

theorem OAI.Problem358.TripleCell.linearIndependent_slopes_of_tie line 297

Source documentation

The two tie-plane normals at a triple tie are linearly independent whenever all three affine branches are strictly active somewhere.

theorem linearIndependent_slopes_of_tie {y0 y1 y2 z : V} {c0 c1 c2 : ℝ}
    (hf : ∃ x, score y1 c1 x < score y0 c0 x ∧ score y2 c2 x < score y0 c0 x)
    (hg : ∃ x, score y0 c0 x < score y1 c1 x ∧ score y2 c2 x < score y1 c1 x)
    (hh : ∃ x, score y0 c0 x < score y2 c2 x ∧ score y1 c1 x < score y2 c2 x)
    (h01 : score y0 c0 z = score y1 c1 z)
    (h02 : score y0 c0 z = score y2 c2 z) :
    LinearIndependent ℝ ![y0 - y1, y0 - y2] := by
…

Mentions: OAI.Problem358.TripleCell.score

theorem OAI.Problem358.TripleCell.exists_tangent_inner_ne_zero line 317
Source documentation
A vector outside a line is detected by some vector tangent to its orthogonal plane.
```
theorem exists_tangent_inner_ne_zero {u v : V}
    (h : ∀ r : ℝ, r • u ≠ v) :
    ∃ w : (ℝ ∙ u)ᗮ, ⟪(w : V), v⟫ ≠ 0 := by
…
```

theorem OAI.Problem358.TripleCell.tangent_inner_zero_null line 331

Source documentation

The second independent tie normal cuts out a null set for Haar measure on the first tie plane's tangent vector space.

theorem tangent_inner_zero_null [FiniteDimensional ℝ V]
    [MeasurableSpace V] [BorelSpace V] {u v : V}
    (h : ∀ r : ℝ, r • u ≠ v)
    (μ : MeasureTheory.Measure ((ℝ ∙ u)ᗮ)) [μ.IsAddHaarMeasure] :
    μ {w : (ℝ ∙ u)ᗮ | ⟪(w : V), v⟫ = 0} = 0 := by
…

theorem OAI.Problem358.TripleCell.tangent_inner_level_null line 350

Source documentation

Every affine level of the second independent normal is surface-null.

theorem tangent_inner_level_null [FiniteDimensional ℝ V]
    [MeasurableSpace V] [BorelSpace V] {u v : V}
    (h : ∀ r : ℝ, r • u ≠ v)
    (μ : MeasureTheory.Measure ((ℝ ∙ u)ᗮ)) [μ.IsAddHaarMeasure] (t : ℝ) :
    μ {w : (ℝ ∙ u)ᗮ | ⟪(w : V), v⟫ = t} = 0 := by
…

theorem OAI.Problem358.TripleCell.triple_tie_surface_null line 373

Source documentation

The common tie locus of three active cells is surface-null in a tie plane, parametrized at any common tie point.

theorem triple_tie_surface_null [FiniteDimensional ℝ V]
    [MeasurableSpace V] [BorelSpace V] {y0 y1 y2 z : V} {c0 c1 c2 : ℝ}
    (hf : ∃ x, score y1 c1 x < score y0 c0 x ∧ score y2 c2 x < score y0 c0 x)
    (hg : ∃ x, score y0 c0 x < score y1 c1 x ∧ score y2 c2 x < score y1 c1 x)
    (hh : ∃ x, score y0 c0 x < score y2 c2 x ∧ score y1 c1 x < score y2 c2 x)
    (h01 : score y0 c0 z = score y1 c1 z)
    (h02 : score y0 c0 z = score y2 c2 z)
    (μ : MeasureTheory.Measure ((ℝ ∙ (y0 - y1))ᗮ)) [μ.IsAddHaarMeasure] :
    μ {w : (ℝ ∙ (y0 - y1))ᗮ |
      score y0 c0 (z + (w : V)) = score y2 c2 (z + (w : V))} = 0 := by
…

Mentions: OAI.Problem358.TripleCell.score

theorem OAI.Problem358.TripleCell.triple_tie_surface_null_of_first_tie line 395

Source documentation

The triple tie locus is surface-null when the first tie hyperplane is parametrized at any of its points; no triple tie need be specified in advance.

theorem triple_tie_surface_null_of_first_tie [FiniteDimensional ℝ V]
    [MeasurableSpace V] [BorelSpace V] {y0 y1 y2 z : V} {c0 c1 c2 : ℝ}
    (hf : ∃ x, score y1 c1 x < score y0 c0 x ∧ score y2 c2 x < score y0 c0 x)
    (hg : ∃ x, score y0 c0 x < score y1 c1 x ∧ score y2 c2 x < score y1 c1 x)
    (hh : ∃ x, score y0 c0 x < score y2 c2 x ∧ score y1 c1 x < score y2 c2 x)
    (h01 : score y0 c0 z = score y1 c1 z)
    (μ : MeasureTheory.Measure ((ℝ ∙ (y0 - y1))ᗮ)) [μ.IsAddHaarMeasure] :
    μ {w : (ℝ ∙ (y0 - y1))ᗮ |
      score y0 c0 (z + (w : V)) = score y2 c2 (z + (w : V))} = 0 := by
…

Mentions: OAI.Problem358.TripleCell.score

theorem OAI.Problem358.TripleCell.ae_no_other_ties_on_interface line 429

Source documentation

On a fixed interface of a finite strictly-active affine family, almost every surface point avoids every other tie hyperplane.

theorem ae_no_other_ties_on_interface {ι : Type*} [Fintype ι]
    [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]
    (y : ι → V) (c : ι → ℝ)
    (hactive : ∀ i, ∃ x, ∀ j, j ≠ i → score (y j) (c j) x < score (y i) (c i) x)
    {i j : ι} (hij : i ≠ j) {z : V}
    (htie : score (y i) (c i) z = score (y j) (c j) z)
    (μ : MeasureTheory.Measure ((ℝ ∙ (y i - y j))ᗮ)) [μ.IsAddHaarMeasure] :
    ∀ᵐ w : (ℝ ∙ (y i - y j))ᗮ ∂μ, ∀ k, k ≠ i → k ≠ j →
      score (y i) (c i) (z + (w : V)) ≠ score (y k) (c k) (z + (w : V)) := by
…

Mentions: OAI.Problem358.TripleCell.score

def OAI.Problem358.GenericSegment.affineScore line 471
lemma OAI.Problem358.GenericSegment.affineScore_combination line 473

theorem OAI.Problem358.GenericSegment.segment_avoids_common_zero_of_det_ne_zero line 481

Source documentation

A nonzero endpoint determinant excludes a simultaneous affine zero on the entire segment, including its endpoints.

theorem segment_avoids_common_zero_of_det_ne_zero
    {v w p q : V} {c d : ℝ}
    (hdet : affineScore v c p * affineScore w d q -
      affineScore w d p * affineScore v c q ≠ 0) :
    ∀ x ∈ segment ℝ p q,
      ¬ (affineScore v c x = 0 ∧ affineScore w d x = 0) := by
…

Mentions: OAI.Problem358.GenericSegment.affineScore

theorem OAI.Problem358.GenericSegment.determinant_normal_ne_zero line 502
Source documentation
For independent normals, the endpoint determinant is a nonconstant affine function of the second endpoint, provided the first endpoint avoids the first hyperplane.
```
theorem determinant_normal_ne_zero {v w p : V} {c d : ℝ}
    (hvw : LinearIndependent ℝ ![v, w]) (hp : affineScore v c p ≠ 0) :
    affineScore v c p • w - affineScore w d p • v ≠ 0 := by
…
```
Mentions: OAI.Problem358.GenericSegment.affineScore
lemma OAI.Problem358.GenericSegment.determinant_eq_affine line 510

theorem OAI.Problem358.GenericSegment.ae_endpoint_determinant_ne_zero line 524

Source documentation

The exceptional second endpoints for a fixed independent pair lie on a single Haar-null affine hyperplane.

theorem ae_endpoint_determinant_ne_zero {v w p : V} {c d : ℝ}
    (hvw : LinearIndependent ℝ ![v, w]) (hp : affineScore v c p ≠ 0) :
    ∀ᵐ q ∂μ, affineScore v c p * affineScore w d q -
      affineScore w d p * affineScore v c q ≠ 0 := by
…

Mentions: OAI.Problem358.GenericSegment.affineScore

theorem OAI.Problem358.GenericSegment.ae_segment_avoids_common_zeros line 540

Source documentation

A generic segment from a fixed endpoint avoids every member of a countable family of codimension-two affine intersections.

theorem ae_segment_avoids_common_zeros {ι : Type*} [Countable ι]
    (v w : ι → V) (c d : ι → ℝ) {p : V}
    (hvw : ∀ i, LinearIndependent ℝ ![v i, w i])
    (hp : ∀ i, affineScore (v i) (c i) p ≠ 0) :
    ∀ᵐ q ∂μ, ∀ i, ∀ x ∈ segment ℝ p q,
      ¬ (affineScore (v i) (c i) x = 0 ∧
        affineScore (w i) (d i) x = 0) := by
…

Mentions: OAI.Problem358.GenericSegment.affineScore

theorem OAI.Problem358.GenericSegment.exists_endpoint_in_open_avoiding_common_zeros line 558

Source documentation

In particular one can choose the second endpoint in any prescribed nonempty open region, as needed when connecting strict cell interiors.

theorem exists_endpoint_in_open_avoiding_common_zeros {ι : Type*} [Countable ι]
    (v w : ι → V) (c d : ι → ℝ) {p : V} {U : Set V}
    (hvw : ∀ i, LinearIndependent ℝ ![v i, w i])
    (hp : ∀ i, affineScore (v i) (c i) p ≠ 0)
    (hU : IsOpen U) (hUne : U.Nonempty) :
    ∃ q ∈ U, ∀ i, ∀ x ∈ segment ℝ p q,
      ¬ (affineScore (v i) (c i) x = 0 ∧
        affineScore (w i) (d i) x = 0) := by
…

Mentions: OAI.Problem358.GenericSegment.affineScore

def OAI.Problem358.TripleTieAvoidance.tieSpace line 581
Source documentation
The equality hyperplane of two affine scores.
```
def tieSpace (y z : V) (a b : ℝ) : AffineSubspace ℝ V :=
…
```
theorem OAI.Problem358.TripleTieAvoidance.mem_tieSpace line 584
theorem OAI.Problem358.TripleTieAvoidance.tieSpace_ne_top line 589
def OAI.Problem358.TripleTieAvoidance.tripleSpace line 600
Source documentation
The common equality locus of three affine scores.
```
def tripleSpace (y : Fin 3 → V) (c : Fin 3 → ℝ) : AffineSubspace ℝ V :=
…
```
theorem OAI.Problem358.TripleTieAvoidance.mem_tripleSpace line 603

theorem OAI.Problem358.TripleTieAvoidance.tripleSpace_codimension line 611

Source documentation

Strict activity of each branch forces every nonempty triple tie to have codimension at least two. Empty loci satisfy the same bound in dimension at least two.

theorem tripleSpace_codimension [FiniteDimensional ℝ V]
    (hd : 2 ≤ Module.finrank ℝ V) (y : Fin 3 → V) (c : Fin 3 → ℝ)
    (hactive : ∀ i, ∃ x, ∀ j, j ≠ i →
      TripleCell.score (y j) (c j) x < TripleCell.score (y i) (c i) x) :
    Module.finrank ℝ (tripleSpace y c).direction + 1 < Module.finrank ℝ V := by
…

Mentions: OAI.Problem358.TripleCell.score, OAI.Problem358.TripleTieAvoidance.tripleSpace

abbrev OAI.Problem358.TripleTieAvoidance.PairIndex line 649
abbrev OAI.Problem358.TripleTieAvoidance.TripleIndex line 650
def OAI.Problem358.TripleTieAvoidance.NoPairTies line 654
Source documentation
No two affine scores agree at the point.
```
def NoPairTies (y : ι → V) (c : ι → ℝ) (x : V) : Prop :=
…
```
def OAI.Problem358.TripleTieAvoidance.NoTripleTies line 658
Source documentation
No three distinct affine scores agree at the point.
```
def NoTripleTies (y : ι → V) (c : ι → ℝ) (x : V) : Prop :=
…
```

theorem OAI.Problem358.TripleTieAvoidance.exists_line_no_triple_ties line 665

Source documentation

Two prescribed nonempty open regions contain endpoints of a line avoiding every triple tie of a finite strictly active affine family.

theorem exists_line_no_triple_ties [FiniteDimensional ℝ V]
    [MeasurableSpace V] [BorelSpace V]
    (μ : Measure V) [IsAddHaarMeasure μ] (hd : 2 ≤ Module.finrank ℝ V)
    (y : ι → V) (c : ι → ℝ)
    (hactive : ∀ i, ∃ x, ∀ j, j ≠ i →
      TripleCell.score (y j) (c j) x < TripleCell.score (y i) (c i) x)
    {U W : Set V} (hU : IsOpen U) (hUne : U.Nonempty)
    (hW : IsOpen W) (hWne : W.Nonempty) :
    ∃ p ∈ U, ∃ q ∈ W, NoPairTies y c p ∧ NoPairTies y c q ∧
      ∀ t : ℝ, NoTripleTies y c (AffineMap.lineMap p q t) := by
…

Mentions: OAI.Problem358.TripleCell.score, OAI.Problem358.TripleTieAvoidance.NoPairTies, OAI.Problem358.TripleTieAvoidance.NoTripleTies

def OAI.Problem358.TripleTieAvoidance.strictRegion line 721
Source documentation
The interior region on which one affine score is strictly maximal.
```
def strictRegion (K : Set V) (y : ι → V) (c : ι → ℝ) (i : ι) : Set V :=
…
```
theorem OAI.Problem358.TripleTieAvoidance.isOpen_strictRegion line 725

theorem OAI.Problem358.TripleTieAvoidance.exists_segment_between_strict_regions line 746

Source documentation

The general-position segment needed for positive-facet connectivity: its endpoints are in prescribed strict cells, every point lies in the interior of the convex source, and no three affine scores agree anywhere on it.

theorem exists_segment_between_strict_regions [FiniteDimensional ℝ V]
    [MeasurableSpace V] [BorelSpace V]
    (μ : Measure V) [IsAddHaarMeasure μ] (hd : 2 ≤ Module.finrank ℝ V)
    (K : Set V) (hK : Convex ℝ K) (y : ι → V) (c : ι → ℝ)
    (hactive : ∀ i, (strictRegion K y c i).Nonempty) (i j : ι) :
    ∃ p ∈ strictRegion K y c i, ∃ q ∈ strictRegion K y c j,
      segment ℝ p q ⊆ interior K ∧
        ∀ x ∈ segment ℝ p q, NoTripleTies y c x := by
…

Mentions: OAI.Problem358.TripleTieAvoidance.strictRegion, OAI.Problem358.TripleTieAvoidance.NoTripleTies