GenericPosition.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Generic vertex positions for the piecewise-linear continuation argument.

lemma OAI.SharpLiebThirring.PLParity.dense_compl_proper_submodule line 26
lemma OAI.SharpLiebThirring.PLParity.dense_linearIndependent_fin line 33
lemma OAI.SharpLiebThirring.PLParity.dense_linearIndependent line 63
def OAI.SharpLiebThirring.PLParity.sumFinSuccEmbedding line 78
Source documentation
Put a new extension vector before the previous extension vectors.
```
def sumFinSuccEmbedding (ι : Type u70) (n : ℕ) :
    ι ⊕ Fin (n + 1) ↪ Option (ι ⊕ Fin n) where
…
```
lemma OAI.SharpLiebThirring.PLParity.dense_linearIndependent_extension line 92
lemma OAI.SharpLiebThirring.PLParity.dense_augmented_linearIndependent line 137
lemma OAI.SharpLiebThirring.PLParity.dense_augmentedIndependent_extension_fin line 174
lemma OAI.SharpLiebThirring.PLParity.dense_linearIndependent_extension_fintype line 218
lemma OAI.SharpLiebThirring.PLParity.dense_augmentedIndependent_extension line 239
lemma OAI.SharpLiebThirring.PLParity.affineIndependent_of_augmented line 261
lemma OAI.SharpLiebThirring.PLParity.independent_shift_of_augmented_extra line 271

lemma OAI.SharpLiebThirring.PLParity.dense_independent_shift line 285

Source documentation

A generic root avoids the affine hull of every prescribed independent proper face. This permits an initial zero inside exactly one maximal flag.

lemma dense_independent_shift {ι : Type u80} [Fintype ι] (v : ι → V)
    (hv : LinearIndependent ℝ (fun i ↦ ((1 : ℝ), v i)))
    (hn : Fintype.card ι ≤ Module.finrank ℝ V) :
    Dense {a : V | LinearIndependent ℝ (fun i ↦ v i - a)} := by
…

lemma OAI.SharpLiebThirring.PLParity.isOpen_independent_shift line 303

lemma OAI.SharpLiebThirring.PLParity.positive_barycentric_neighborhood line 310

Source documentation

Positive barycentric coordinates remain positive on a neighborhood when an augmented vertex family is a basis.

lemma positive_barycentric_neighborhood {ι : Type u82} [Fintype ι]
    (v : ι → V) (hv : LinearIndependent ℝ (fun i ↦ ((1 : ℝ), v i)))
    (hn : Fintype.card ι = Module.finrank ℝ V + 1)
    (w : ι → ℝ) (hw : ∀ i, 0 < w i) (hs : ∑ i, w i = 1) :
    ∃ U : Set V, IsOpen U ∧ (∑ i, w i • v i) ∈ U ∧
      ∀ x ∈ U, ∃ z : ι → ℝ, (∀ i, 0 < z i) ∧ ∑ i, z i = 1 ∧ ∑ i, z i • v i = x := by
…

def OAI.SharpLiebThirring.PLParity.vertexEvaluation line 350
Source documentation
On distinct vertex orbits, equivariant vertex values may be varied independently.
```
def vertexEvaluation (e : ι → Q) (A : ι → V ≃ₗ[ℝ] V) :
    (Q → V) →ₗ[ℝ] (ι → V) where
…
```
lemma OAI.SharpLiebThirring.PLParity.vertexEvaluation_surjective line 357
lemma OAI.SharpLiebThirring.PLParity.vertexEvaluation_isOpenMap line 366
lemma OAI.SharpLiebThirring.PLParity.vertexEvaluation_continuous line 372
lemma OAI.SharpLiebThirring.PLParity.dense_vertex_linearlyIndependent line 376
lemma OAI.SharpLiebThirring.PLParity.dense_vertex_augmentedIndependent line 381
lemma OAI.SharpLiebThirring.PLParity.isOpen_vertex_linearlyIndependent line 386
lemma OAI.SharpLiebThirring.PLParity.isOpen_vertex_augmentedIndependent line 390

lemma OAI.SharpLiebThirring.PLParity.dense_vertex_independent_extension line 398

Source documentation

Genericity may be imposed while retaining an independent prescribed part. This is used for the initial boundary of the continuation cylinder.

lemma dense_vertex_independent_extension {κ : Type u85} [Fintype κ]
    (v : κ → V) (hv : LinearIndependent ℝ v)
    (e : ι → Q) (he : Function.Injective e) (A : ι → V ≃ₗ[ℝ] V)
    (hn : Fintype.card κ + Fintype.card ι ≤ Module.finrank ℝ V) :
    Dense {w : Q → V | LinearIndependent ℝ (Sum.elim v (vertexEvaluation e A w))} :=
…

Mentions: OAI.SharpLiebThirring.PLParity.vertexEvaluation

lemma OAI.SharpLiebThirring.PLParity.dense_vertex_augmented_extension line 406
lemma OAI.SharpLiebThirring.PLParity.isOpen_vertex_independent_extension line 415
lemma OAI.SharpLiebThirring.PLParity.isOpen_vertex_augmented_extension line 424
def OAI.SharpLiebThirring.PLParity.mixedVertexEvaluation line 439
Source documentation
Extend vertex values on the free orbits while retaining the prescribed orbits.
```
def mixedVertexEvaluation (P : Q → Prop) (b : Q → V) (e : ι → Q)
    (A : ι → V ≃ₗ[ℝ] V) (a : {q // ¬ P q} → V) (i : ι) : V :=
…
```
lemma OAI.SharpLiebThirring.PLParity.mixedVertexEvaluation_continuous line 444
lemma OAI.SharpLiebThirring.PLParity.isOpen_mixed_independent line 455
lemma OAI.SharpLiebThirring.PLParity.isOpen_mixed_augmented line 461
lemma OAI.SharpLiebThirring.PLParity.dense_mixed_independent line 469
lemma OAI.SharpLiebThirring.PLParity.dense_mixed_augmented line 498

lemma OAI.SharpLiebThirring.PLParity.dense_finite_conditions line 534

Source documentation

Finitely many open genericity conditions can be imposed at once.

lemma dense_finite_conditions {X : Type u89} {κ : Type u90} [TopologicalSpace X] [Finite κ]
    (P : κ → X → Prop) (ho : ∀ k, IsOpen {x | P k x}) (hd : ∀ k, Dense {x | P k x}) :
    Dense {x | ∀ k, P k x} := by
…

lemma OAI.SharpLiebThirring.PLParity.exists_mixed_generic line 544

Source documentation

Arbitrarily small generic perturbations of finitely many equivariant vertex values, with an already generic prescribed part retained exactly. The orbit labels and transports are abstract here; a free finite group action supplies them.

lemma exists_mixed_generic
    {Q : Type u91} {W : Type u92} {T₁ : Type u93} {T₂ : Type u94} [Fintype Q] [Fintype W] [Fintype T₁] [Fintype T₂]
    (J₁ : T₁ → Type u191) (J₂ : T₂ → Type u192) [∀ t, Fintype (J₁ t)] [∀ t, Fintype (J₂ t)]
    (P : Q → Prop) (b : Q → V) (e : W → Q) (A : W → V ≃ₗ[ℝ] V)
    (v₁ : ∀ t, J₁ t → W) (v₂ : ∀ t, J₂ t → W)
    (he₁ : ∀ t, Function.Injective (e ∘ v₁ t))
    (he₂ : ∀ t, Function.Injective (e ∘ v₂ t))
    (hf₁ : ∀ t, LinearIndependent ℝ
      (fun i : {i // P (e (v₁ t i))} ↦ A (v₁ t i.val) (b (e (v₁ t i.val)))))
    (hf₂ : ∀ t, LinearIndependent ℝ
      (fun i : {i // P (e (v₂ t i))} ↦ ((1 : ℝ), A (v₂ t i.val) (b (e (v₂ t i.val))))))
    (hc₁ : ∀ t, Fintype.card (J₁ t) ≤ Module.finrank ℝ V)
…