OAI/Analysis/LiebThirring/EquivariantFlags.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpLiebThirring.PLParity.Orbit line 21
2. lemma OAI.SharpLiebThirring.PLParity.assignment_orbit_smul line 24
3. def OAI.SharpLiebThirring.PLParity.assignmentEquiv line 28
4. def OAI.SharpLiebThirring.PLParity.orbitLabel line 46
5. def OAI.SharpLiebThirring.PLParity.orbitTransport line 47
6. lemma OAI.SharpLiebThirring.PLParity.assignment_reconstruct line 49
7. lemma OAI.SharpLiebThirring.PLParity.assignment_symm_smul line 52
8. lemma OAI.SharpLiebThirring.PLParity.orbitLabel_smul line 59
9. lemma OAI.SharpLiebThirring.PLParity.orbitTransport_smul line 62
10. lemma OAI.SharpLiebThirring.PLParity.orbitLabel_eq_mk line 65
11. def OAI.SharpLiebThirring.PLParity.equivariantAssignment line 73
12. lemma OAI.SharpLiebThirring.PLParity.equivariantAssignment_smul line 77
13. lemma OAI.SharpLiebThirring.PLParity.equivariantAssignment_recovers line 83
14. lemma OAI.SharpLiebThirring.PLParity.exists_equivariant_generic line 90

    Source documentation

    Free finite group actions admit arbitrarily close equivariant generic vertex values, while retaining a prescribed invariant family exactly.

    lemma exists_equivariant_generic [Fintype X]
        {T₁ : Type u98} {T₂ : Type u99} [Fintype T₁] [Fintype T₂]
        (J₁ : T₁ → Type u193) (J₂ : T₂ → Type u194) [∀ t, Fintype (J₁ t)] [∀ t, Fintype (J₂ t)]
        (P : X → Prop) (hP : ∀ g : G, ∀ x, P (g • x) ↔ P x)
        (b : X → V) (hb : ∀ g : G, ∀ x, b (g • x) = ρ g (b x))
        (v₁ : ∀ t, J₁ t → X) (v₂ : ∀ t, J₂ t → X)
        (he₁ : ∀ t, Function.Injective (orbitLabel (G := G) ∘ v₁ t))
    …

    Mentions: OAI.SharpLiebThirring.PLParity.orbitLabel

15. lemma OAI.SharpLiebThirring.CubeFlags.card_omit_one_le line 160
16. lemma OAI.SharpLiebThirring.CubeFlags.card_omit_two_le line 165
17. lemma OAI.SharpLiebThirring.CubeFlags.generic_on_complex line 178

    Source documentation

    General position on all facets of an invariant finite cubical complex, retaining an already independent invariant part of its vertex data.

    lemma generic_on_complex {n : ℕ} (H : Subgroup (Signs n)) (D : SubMulAction H (Flag n))
        [Fintype D] [IsCancelSMul H (vertices H D)]
        {V : Type u100} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
        (ρ : H →* (V ≃ₗ[ℝ] V)) (hc : n = Module.finrank ℝ V + 1)
        (P : vertices H D → Prop) (hP : ∀ s : H, ∀ z, P (s • z) ↔ P z)
        (b : vertices H D → V) (hb : ∀ s : H, ∀ z, b (s • z) = ρ s (b z))
        (haug : ∀ F : D, ∀ j : Fin (n + 1), LinearIndependent ℝ
          (fun k : {k : {k : Fin (n + 1) // k ≠ j} // P (flagVertex H D F k.val)} ↦
            ((1 : ℝ), b (flagVertex H D F k.val.val))))
        (hvec : ∀ F : D, ∀ i j : Fin (n + 1), i ≠ j → LinearIndependent ℝ
          (fun k : {k : {k : Fin (n + 1) // k ≠ i ∧ k ≠ j} // P (flagVertex H D F k.val)} ↦
            b (flagVertex H D F k.val.val)))
    …

    Mentions: OAI.SharpLiebThirring.CubeFlags.Signs, OAI.SharpLiebThirring.CubeFlags.Flag, OAI.SharpLiebThirring.CubeFlags.vertices, OAI.SharpLiebThirring.CubeFlags.flagVertex

18. def OAI.SharpLiebThirring.CubeFlags.spatial line 236
19. def OAI.SharpLiebThirring.CubeFlags.embedSpatial line 241
20. lemma OAI.SharpLiebThirring.CubeFlags.spatial_embed line 246
21. lemma OAI.SharpLiebThirring.CubeFlags.embed_spatial_of_time_zero line 251
22. lemma OAI.SharpLiebThirring.CubeFlags.augmented_spatial_independent line 256
23. lemma OAI.SharpLiebThirring.CubeFlags.augmented_scale_independent line 270
24. def OAI.SharpLiebThirring.CubeFlags.bottomSeed line 283

    Source documentation

    A bottom flag with its cube chosen within one mesh of any given spatial point.

    def bottomSeed {d : ℕ} (h : ℝ) (p : Fin d → ℝ) : Flag (d + 1) where
    …

    Mentions: OAI.SharpLiebThirring.CubeFlags.Flag

25. lemma OAI.SharpLiebThirring.CubeFlags.bottomSeed_time line 288
26. lemma OAI.SharpLiebThirring.CubeFlags.bottomSeed_dist_center line 293
27. lemma OAI.SharpLiebThirring.CubeFlags.bottomSeed_dist_point line 314