PointExpansion.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite-point incidence avoidance and expansion inequalities.

def OAI.Kaplansky.Incidence.PointBad line 17
theorem OAI.Kaplansky.Incidence.pointBad_null line 22
Source documentation
The full bad locus over a point is null, across ALL s-planes and t-planes. The countable graph cover is constructed from the actual Grassmann spaces.
```
theorem pointBad_null [MeasurableSpace (TupleOperators q s k t l)]
    [BorelSpace (TupleOperators q s k t l)] (hgap : s*k+t*l<q*s*l) :
    μH[finrank ℝ (TupleOperators q s k t l)] (PointBad (q := q) (s := s) (k := k) (t := t) (l := l))=0 := by
…
```
Mentions: OAI.Kaplansky.Incidence.TupleOperators, OAI.Kaplansky.Incidence.PointBad
theorem OAI.Kaplansky.Incidence.exists_point_incidence_avoiding line 46
Source documentation
Existence for the point version, for a fixed forbidden pair of dimensions. This is a constructed tuple avoiding every actual pair of subspaces.
```
theorem exists_point_incidence_avoiding (hgap : s*k+t*l<q*s*l) :
    ∃ T : TupleOperators q s k t l,
      ∀ (P : Grassmann s k) (Q : Grassmann t l), ¬ ∀ i, ∀ x ∈ P.val, T i x ∈ Q.val := by
…
```
Mentions: OAI.Kaplansky.Incidence.TupleOperators

theorem OAI.Kaplansky.Incidence.exists_super_finrank line 69

Source documentation

Extend any subspace to a prescribed intermediate dimension.

theorem exists_super_finrank {E : Type*} [AddCommGroup E] [Module ℂ E]
    [FiniteDimensional ℂ E] (S : Submodule ℂ E) {n : ℕ}
    (hSn : finrank ℂ S≤n) (hn : n≤finrank ℂ E) :
    ∃ U : Submodule ℂ E, S≤U ∧ finrank ℂ U=n := by
…

theorem OAI.Kaplansky.Incidence.exists_point_expanding_fixed_rank line 90
abbrev OAI.Kaplansky.Incidence.MatrixTuple line 114
def OAI.Kaplansky.Incidence.RankBad line 116
theorem OAI.Kaplansky.Incidence.rankBad_null line 120
theorem OAI.Kaplansky.Incidence.exists_point_incidence_tuple line 137
theorem OAI.Kaplansky.Incidence.point_dimension_inequality_iff line 168