Avoidance.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Avoidance of lower-dimensional incidence images in local manifold charts.

theorem OAI.Kaplansky.Incidence.smoothOn_open_dimH_image_le line 19

Source documentation

Local smoothness on an open coordinate domain suffices; convexity and compactness of the whole coordinate domain are not assumptions.

theorem smoothOn_open_dimH_image_le {E F : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    {f : E → F} {s : Set E} (hs : IsOpen s) (hf : ContDiffOn ℝ 1 f s) :
    dimH (f '' s) ≤ finrank ℝ E := by
…

theorem OAI.Kaplansky.Incidence.smoothOn_open_image_null line 32

Source documentation

The lower-dimensional smooth image is null for top-dimensional Hausdorff measure, which is an additive Haar measure on the target.

theorem smoothOn_open_image_null {E F : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F]
    [MeasurableSpace F] [BorelSpace F]
    {f : E → F} {s : Set E} (hs : IsOpen s) (hf : ContDiffOn ℝ 1 f s)
    (hd : finrank ℝ E < finrank ℝ F) : μH[finrank ℝ F] (f '' s)=0 := by
…

theorem OAI.Kaplansky.Incidence.exists_outside_countable_smooth_images line 45

Source documentation

A countable family of smaller-dimensional smooth coordinate images cannot exhaust the parameter space. The null-image claims are proved here.

theorem exists_outside_countable_smooth_images {ι F : Type*} [Countable ι]
    [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F]
    (E : ι → Type*) [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace ℝ (E i)]
    [∀ i, FiniteDimensional ℝ (E i)] (s : ∀ i, Set (E i)) (f : ∀ i, E i → F)
    (hs : ∀ i, IsOpen (s i)) (hf : ∀ i, ContDiffOn ℝ 1 (f i) (s i))
    (hd : ∀ i, finrank ℝ (E i)<finrank ℝ F) :
    ∃ v : F, ∀ i, v ∉ f i '' s i := by
…

def OAI.Kaplansky.localChartDomain line 82
Source documentation
The actual chart domain restricted to a bundle trivializing open set.
```
def localChartDomain (U : B → Set B) (x : B) : Set X :=
…
```
theorem OAI.Kaplansky.localChartDomain_open line 86
theorem OAI.Kaplansky.localChartDomain_smooth line 90

theorem OAI.Kaplansky.exists_countable_local_chart_cover line 100

Source documentation

A countable choice of actual base charts covers the manifold while also respecting the prescribed open neighborhoods.

theorem exists_countable_local_chart_cover [LindelofSpace B]
    (U : B → Set B) (hU : ∀ x, IsOpen (U x)) (hxU : ∀ x, x ∈ U x) :
    ∃ c : Set B, c.Countable ∧ ∀ y, ∃ x ∈ c,
      y ∈ U x ∧ y ∈ (chartAt X x).source ∧
      (chartAt X x) y ∈ localChartDomain U x ∧
      (chartAt X x).symm ((chartAt X x) y)=y := by
…

Mentions: OAI.Kaplansky.localChartDomain

theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.fromModel_contDiffAt line 134
def OAI.Kaplansky.SmoothKernel.SurjectiveFamily.kernelParameterization line 142
theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.kernelParameterization_smooth line 144
theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.exists_countable_baseSet_cover line 154
theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.kernel_incidence_image_null line 164
Source documentation
The image of the ACTUAL kernel incidence subset is null. The proof uses a countable cover of the constructed kernel charts, not a null-image premise.
```
theorem kernel_incidence_image_null [MeasurableSpace V] [BorelSpace V]
    (hA : ContDiff ℝ ∞ A.map)
    (hd : finrank ℝ (X × KernelModel V W)<finrank ℝ V) :
    μH[finrank ℝ V] {v : V | ∃ x, A.map x v=0}=0 := by
…
```
Mentions: OAI.Kaplansky.SmoothKernel.KernelModel
theorem OAI.Kaplansky.SmoothKernel.SurjectiveFamily.exists_avoiding_kernels line 183
Source documentation
A parameter outside every actual kernel exists under the dimension gap.
```
theorem exists_avoiding_kernels (hA : ContDiff ℝ ∞ A.map)
    (hd : finrank ℝ (X × KernelModel V W)<finrank ℝ V) :
    ∃ v : V, ∀ x, A.map x v ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.SmoothKernel.KernelModel
theorem OAI.Kaplansky.Incidence.evaluation_target_rank_le line 210
theorem OAI.Kaplansky.Incidence.graph_incidence_dimension_gap line 219

theorem OAI.Kaplansky.Incidence.graph_incidence_image_null line 230

Source documentation

On one pair of Grassmann graph charts, the actual bad-parameter locus is null under exactly the incidence dimension gap.

theorem graph_incidence_image_null [MeasurableSpace V] [BorelSpace V]
    (he : ContDiff ℝ ∞ ev) (hs : ∀ y, Function.Surjective (ev y))
    (hY : finrank ℝ Y=2*h) (hgap : h+s*k+t*l<q*s*l) :
    μH[finrank ℝ V] {v : V | ∃ (y : Y) (a : GraphSlope s k) (b : GraphSlope t l), ∀ i, ∀ x ∈ a.toLinearMap.graph,
      ev y v i x ∈ b.toLinearMap.graph}=0 := by
…

theorem OAI.Kaplansky.Incidence.exists_avoiding_graph_incidence line 246

Source documentation

A tuple is constructed outside all incidence kernels in these charts; it is not supplied as a premise. Full Grassmann coverage is a separate step.

theorem exists_avoiding_graph_incidence (he : ContDiff ℝ ∞ ev)
    (hs : ∀ y, Function.Surjective (ev y)) (hY : finrank ℝ Y=2*h)
    (hgap : h+s*k+t*l<q*s*l) :
    ∃ v : V, ∀ y (a : GraphSlope s k) (b : GraphSlope t l),
      ¬ ∀ i, ∀ x ∈ a.toLinearMap.graph, ev y v i x ∈ b.toLinearMap.graph := by
…

abbrev OAI.Kaplansky.Incidence.TupleOperators line 266
def OAI.Kaplansky.Incidence.frameEvaluationLinear line 268
def OAI.Kaplansky.Incidence.frameEvaluation line 285
theorem OAI.Kaplansky.Incidence.frameEvaluation_apply line 289
theorem OAI.Kaplansky.Incidence.frameEvaluation_surjective line 293
theorem OAI.Kaplansky.Incidence.frame_incidence_iff line 304
def OAI.Kaplansky.Incidence.ChartBad line 318
theorem OAI.Kaplansky.Incidence.chartBad_null line 324
Source documentation
The actual bad tuples in any pair of graph charts form a null set over a point; no restriction is placed on the positions of the two charts.
```
theorem chartBad_null (F : GraphFrame s k) (G : GraphFrame t l)
    [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)] (ChartBad (q := q) F G)=0 := by
…
```
Mentions: OAI.Kaplansky.Incidence.TupleOperators, OAI.Kaplansky.Incidence.ChartBad