OAI/Analysis/LiebThirring/FreeLocus.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.PLParity.small_norm_near_zeros line 32

   Source documentation

   On a compact domain, sufficiently small values lie in any open neighborhood of the zero set. This is not an existence assumption about zeros.

   lemma small_norm_near_zeros {C U : Set E} (hC : IsCompact C) (hU : IsOpen U)
       (f : E → V) (hf : ContinuousOn f C) (hzero : ∀ x ∈ C, f x = 0 → x ∈ U) :
       ∃ ε > 0, ∀ x ∈ C, ‖f x‖ < ε → x ∈ U := by
   …

2. lemma OAI.SharpLiebThirring.PLParity.norm_of_convex_zero line 51
3. lemma OAI.SharpLiebThirring.PLParity.norm_of_approximate_convex_zero line 66
4. def OAI.SharpLiebThirring.PLParity.freeLocus line 79
5. lemma OAI.SharpLiebThirring.PLParity.freeLocus_smul line 81
6. def OAI.SharpLiebThirring.PLParity.freeSubMulAction line 90
7. instance OAI.SharpLiebThirring.PLParity.(instance at line 94) line 94
8. lemma OAI.SharpLiebThirring.PLParity.isOpen_freeLocus line 103
9. lemma OAI.SharpLiebThirring.PLParity.compact_free_tube line 124
10. def OAI.SharpLiebThirring.CubeFlags.Flag.combination line 135
11. lemma OAI.SharpLiebThirring.CubeFlags.Flag.combination_neighbor line 138
12. lemma OAI.SharpLiebThirring.CubeFlags.Flag.dist_combination_scaled_center line 152
13. lemma OAI.SharpLiebThirring.CubeFlags.Flag.dist_combination_gridPoint line 158
14. lemma OAI.SharpLiebThirring.CubeFlags.nearCylinder_combination_cthickening line 164
15. lemma OAI.SharpLiebThirring.CubeFlags.cellHit_weights line 175
16. lemma OAI.SharpLiebThirring.CubeFlags.norm_at_mesh_zero line 186

    Source documentation

    A PL zero gives a small value of the continuous map at its geometric point.

    lemma norm_at_mesh_zero {n : ℕ} (H : Subgroup (Signs n)) (D : SubMulAction H (Flag n))
        {V : Type u125} [NormedAddCommGroup V] [NormedSpace ℝ V]
        (a : vertices H D → V) (f : (Fin n → ℝ) → V) (h ε δ : ℝ) (hh : 0 ≤ h)
        (C : Set (Fin n → ℝ))
        (ha : ∀ z : vertices H D, dist (a z) (f (gridPoint h z.val)) ≤ ε)
        (hf : ∀ x ∈ C, ∀ y ∈ C, dist x y ≤ h → dist (f x) (f y) ≤ δ)
        (F : D) (w : Fin (n + 1) → ℝ) (hw : ∀ k, 0 ≤ w k) (hs : ∑ k, w k = 1)
        (hz : ∑ k, w k • a (flagVertex H D F k) = 0)
        (hC : F.val.combination h w ∈ C)
        (hp : ∀ k, gridPoint h (F.val.vertex k) ∈ C) :
        ‖f (F.val.combination h w)‖ ≤ ε + δ := by
    …

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

17. lemma OAI.SharpLiebThirring.CubeFlags.neighbor_near_centers_of_combination line 206
18. lemma OAI.SharpLiebThirring.CubeFlags.Flag.combination_time_boundary line 219
19. lemma OAI.SharpLiebThirring.CubeFlags.Flag.combination_eq_sum_gridPoint line 241
20. lemma OAI.SharpLiebThirring.CubeFlags.Signs.smul_sum_real line 246
21. lemma OAI.SharpLiebThirring.CubeFlags.Flag.combination_smul line 253
22. lemma OAI.SharpLiebThirring.CubeFlags.sum_affine_linear line 260
23. lemma OAI.SharpLiebThirring.CubeFlags.cellHit_of_weights line 267
24. lemma OAI.SharpLiebThirring.CubeFlags.affine_sum_on_facet line 277
25. lemma OAI.SharpLiebThirring.CubeFlags.mesh_affine_zero_point line 290
26. lemma OAI.SharpLiebThirring.CubeFlags.model_seed_hit line 319
27. lemma OAI.SharpLiebThirring.CubeFlags.bottom_facet_unique line 348