Intercalate a polyhedron in an open set

LeanCamCombi.lean

@@ -22,8 +22,12 @@ import LeanCamCombi.Mathlib.Algebra.BigOperators.Ring
 import LeanCamCombi.Mathlib.Algebra.Order.BigOperators.LocallyFinite
 import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
 import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
+import LeanCamCombi.Mathlib.Analysis.Convex.Hull
 import LeanCamCombi.Mathlib.Analysis.Convex.Independence
+import LeanCamCombi.Mathlib.Analysis.Convex.Normed
+import LeanCamCombi.Mathlib.Analysis.Convex.Segment
 import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic
+import LeanCamCombi.Mathlib.Analysis.Normed.Group.Basic
 import LeanCamCombi.Mathlib.Combinatorics.Colex
 import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
 import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
@@ -52,6 +56,7 @@ import LeanCamCombi.Mathlib.Order.Sublattice
 import LeanCamCombi.Mathlib.Probability.Independence.Basic
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.Mathlib.RingTheory.Int.Basic
+import LeanCamCombi.Mathlib.Topology.Algebra.Group.Basic
 import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
 import LeanCamCombi.SimplicialComplex.Basic

LeanCamCombi/ConvexContinuous.lean

@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Analysis.Convex.Intrinsic
-import Mathlib.Analysis.Convex.Topology
-import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.Analysis.InnerProductSpace.Basic
+import LeanCamCombi.Mathlib.Analysis.Convex.Normed
+import LeanCamCombi.Mathlib.Analysis.Normed.Group.Basic
+import LeanCamCombi.Mathlib.Topology.Algebra.Group.Basic
 
 /-!
 # Convex functions are continuous
@@ -15,94 +17,16 @@ continuous.
 
 ## TODO
 
-Can this be extended to real normed spaces?
+Define `LocallyLipschitzOn`
 -/
 
-namespace Real
-variable {ε r : ℝ}
-
-open Metric
-
-lemma closedBall_eq_segment (hε : 0 ≤ ε) : closedBall r ε = segment ℝ (r - ε) (r + ε) := by
-  rw [closedBall_eq_Icc, segment_eq_Icc ((sub_le_self _ hε).trans $ le_add_of_nonneg_right hε)]
-
-end Real
-
-section pi
-variable {𝕜 ι : Type*} {E : ι → Type*} [Fintype ι] [LinearOrderedField 𝕜]
-  [Π i, AddCommGroup (E i)] [Π i, Module 𝕜 (E i)] {s : Set ι} {t : Π i, Set (E i)} {f : Π i, E i}
-
-lemma mem_convexHull_pi (h : ∀ i ∈ s, f i ∈ convexHull 𝕜 (t i)) : f ∈ convexHull 𝕜 (s.pi t) :=
-  sorry -- See `mk_mem_convexHull_prod`
-
-@[simp] lemma convexHull_pi (s : Set ι) (t : Π i, Set (E i)) :
-    convexHull 𝕜 (s.pi t) = s.pi (fun i ↦ convexHull 𝕜 (t i)) :=
-  Set.Subset.antisymm (convexHull_min (Set.pi_mono fun _ _ ↦ subset_convexHull _ _) $ convex_pi $
-    fun _ _ ↦ convex_convexHull _ _) fun _ ↦ mem_convexHull_pi
-
-end pi
-
-section
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
-  {s : Set E} {x : E}
-
-open FiniteDimensional Metric Set
-open scoped BigOperators
-
-/-- We can intercalate a polyhedron between an intrinsically open set and one of its elements,
-namely a small enough cube. -/
-lemma IsOpen.exists_mem_intrinsicInterior_convexHull_finset
-  (hs : IsOpen ((↑) ⁻¹' s : Set $ affineSpan ℝ s)) (hx : x ∈ s) :
-  ∃ t : Finset E, x ∈ intrinsicInterior ℝ (convexHull ℝ (t : Set E)) ∧
-    convexHull ℝ (t : Set E) ⊆ s := by
-  classical
-  lift x to affineSpan ℝ s using subset_affineSpan _ _ hx
-  set x : affineSpan ℝ s := x with hx
-  clear_value x
-  subst hx
-  obtain ⟨ε, hε, hεx⟩ := (Metric.nhds_basis_closedBall.1 _).1 (isOpen_iff_mem_nhds.1 hs _ hx)
-  set f : Finset (Fin $ finrank ℝ $ vectorSpan ℝ s) → vectorSpan ℝ s :=
-    fun u ↦ (ε / ∑ i, ‖finBasis ℝ (vectorSpan ℝ s) i‖) • ∑ i, if i ∈ u then
-      finBasis ℝ (vectorSpan ℝ s) i else -finBasis ℝ (vectorSpan ℝ s) i
-      with hf
-  sorry
-  -- set t := Finset.univ.image (fun u, f u +ᵥ x) with ht,
-  -- refine ⟨t, _, (convexHull_min _ $ convex_closedBall _ _).trans hεx⟩,
-  -- { have hf' : isOpen_map (fun w : fin (finrank ℝ E) → ℝ, x + ∑ i, w i • finBasis ℝ E i) := sorry,
-  --   refine interior_maximal _ (hf' _ isOpen_ball) ⟨0, mem_ball_self zero_lt_one,
-  --     by simp only [pi.zero_apply, zero_smul, Finset.sum_const_zero, add_zero]⟩,
-  --   rw image_subset_iff,
-  --   refine ball_subset_closedBall.trans _,
-  --   simp_rw [closedBall_pi _ zero_le_one, Real.closedBall_eq_segment zero_le_one,
-  --     ← convexHull_pair, ← convexHull_pi, pi.zero_apply, zero_sub, zero_add, ht, Finset.coe_image,
-  --     Finset.coe_univ, image_univ],
-  --   refine convexHull_min (fun w hw, subset_convexHull _ _ _) _,
-  --   refine ⟨Finset.univ.filter (fun i ↦ w i = 1), _⟩,
-  --   sorry,
-  --   refine (convex_convexHull _ _).is_linear_preimage _, -- rather need bundled affine preimage
-  --   sorry,
-  -- },
-  -- { have hε' : 0 ≤ ε / finrank ℝ E := by positivity,
-  --   simp_rw [ht, Finset.coe_image, Finset.coe_univ,image_univ, range_subset_iff, mem_closedBall,
-  --     dist_self_add_left],
-  --   rintro u,
-  --   have hE : 0 ≤ ∑ i, ‖finBasis ℝ E i‖ := Finset.sum_nonneg (fun x hx, norm_nonneg _),
-  --   simp_rw [hf, norm_smul, Real.norm_of_nonneg (div_nonneg hε.le hE), div_mul_comm ε,
-  --     mul_le_iff_le_one_left hε],
-  --   refine div_le_one_of_le ((norm_sum_le _ _).trans $ Finset.sum_le_sum fun i _, _) hE,
-  --   rw [apply_ite norm, norm_neg, if_t_t] }
-
-end
-
 open FiniteDimensional Metric Set
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
   {s : Set E} {f : E → ℝ}
 
--- TODO: This proof actually gives local Lipschitz continuity.
--- See `IsOpen.exists_mem_interior_convexHull_finset` for more todo.
 protected lemma ConvexOn.continuousOn (hf : ConvexOn ℝ s f) :
-  ContinuousOn f (intrinsicInterior ℝ s) := by
+    ContinuousOn f (intrinsicInterior ℝ s) := by
   classical
   -- refine isOpen_interior.continuousOn_iff.2 (fun x hx, _),
   -- obtain ⟨t, hxt, hts⟩ := isOpen_interior.exists_mem_interior_convexHull_finset hx,
@@ -115,5 +39,19 @@ protected lemma ConvexOn.continuousOn (hf : ConvexOn ℝ s f) :
   sorry
 
 protected lemma ConcaveOn.continuousOn (hf : ConcaveOn ℝ s f) :
-  ContinuousOn f (intrinsicInterior ℝ s) :=
-sorry
+    ContinuousOn f (intrinsicInterior ℝ s) := by simpa using hf.neg.continuousOn
+
+protected lemma ConvexOn.locallyLipschitz (hf : ConvexOn ℝ univ f) : LocallyLipschitz f := by
+  classical
+  -- refine isOpen_interior.continuousOn_iff.2 (fun x hx, _),
+  -- obtain ⟨t, hxt, hts⟩ := isOpen_interior.exists_mem_interior_convexHull_finset hx,
+  -- set M := t.sup' (convexHull_nonempty_iff.1 $ nonempty.mono interior_subset ⟨x, hxt⟩) f,
+  -- refine metric.continuous_at_iff.2 (fun ε hε, _),
+  -- have : f x ≤ M := le_sup_of_mem_convexHull
+  --   (hf.subset (hts.trans interior_subset) $ convex_convexHull _ _) (interior_subset hxt),
+  -- refine ⟨ε / (M - f x), _, fun y hy, _⟩,
+  -- sorry,
+  sorry
+
+protected lemma ConcaveOn.locallyLipschitz (hf : ConcaveOn ℝ univ f) : LocallyLipschitz f := by
+  simpa using hf.neg.locallyLipschitz

LeanCamCombi/Mathlib/Analysis/Convex/Hull.lean

@@ -0,0 +1,26 @@
+import Mathlib.Analysis.Convex.Hull
+
+section OrderedCommSemiring
+variable {𝕜 E : Type*} [OrderedCommRing 𝕜] [AddCommGroup E] [Module 𝕜 E]
+
+open scoped Pointwise
+
+-- TODO: Turn `convexHull_smul` around
+lemma convexHull_vadd (x : E) (s : Set E) : convexHull 𝕜 (x +ᵥ s) = x +ᵥ convexHull 𝕜 s :=
+  (AffineEquiv.constVAdd 𝕜 _ x).toAffineMap.image_convexHull s |>.symm
+
+end OrderedCommSemiring
+
+section pi
+variable {𝕜 ι : Type*} {E : ι → Type*} [Fintype ι] [LinearOrderedField 𝕜]
+  [Π i, AddCommGroup (E i)] [Π i, Module 𝕜 (E i)] {s : Set ι} {t : Π i, Set (E i)} {f : Π i, E i}
+
+lemma mem_convexHull_pi (h : ∀ i ∈ s, f i ∈ convexHull 𝕜 (t i)) : f ∈ convexHull 𝕜 (s.pi t) :=
+  sorry -- See `mk_mem_convexHull_prod`
+
+@[simp] lemma convexHull_pi (s : Set ι) (t : Π i, Set (E i)) :
+    convexHull 𝕜 (s.pi t) = s.pi (fun i ↦ convexHull 𝕜 (t i)) :=
+  Set.Subset.antisymm (convexHull_min (Set.pi_mono fun _ _ ↦ subset_convexHull _ _) $ convex_pi $
+    fun _ _ ↦ convex_convexHull _ _) fun _ ↦ mem_convexHull_pi
+
+end pi

LeanCamCombi/Mathlib/Analysis/Convex/Normed.lean

@@ -0,0 +1,49 @@
+import Mathlib.Analysis.Convex.Normed
+import Mathlib.Analysis.NormedSpace.AddTorsorBases
+import LeanCamCombi.Mathlib.Analysis.Convex.Hull
+
+open AffineBasis FiniteDimensional Metric Set
+open scoped Pointwise Topology
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
+  {s : Set E} {x : E}
+
+/-- We can intercalate a polyhedron between a point and one of its neighborhoods. -/
+lemma exists_mem_interior_convexHull_finset (hs : s ∈ 𝓝 x) :
+    ∃ t : Finset E, x ∈ interior (convexHull ℝ t : Set E) ∧ convexHull ℝ t ⊆ s := by
+  classical
+  wlog hx : x = 0
+  · obtain ⟨t, ht⟩ := this (s := -x +ᵥ s) (by simpa using vadd_mem_nhds (-x) hs) rfl
+    use x +ᵥ t
+    simpa [subset_set_vadd_iff, mem_vadd_set_iff_neg_vadd_mem, convexHull_vadd, interior_vadd]
+      using ht
+  subst hx
+  obtain ⟨b⟩ := exists_affineBasis_of_finiteDimensional
+    (ι := Fin (finrank ℝ E + 1)) (k := ℝ) (P := E) (by simp)
+  obtain ⟨ε, hε, hεs⟩ := Metric.mem_nhds_iff.1 hs
+  set u : Finset E := -Finset.univ.centroid ℝ b +ᵥ Finset.univ.image b
+  have hu₀ : 0 ∈ interior (convexHull ℝ u : Set E) := by
+    simpa [u, convexHull_vadd, interior_vadd, mem_vadd_set_iff_neg_vadd_mem]
+      using b.centroid_mem_interior_convexHull
+  have hu : u.Nonempty := Finset.nonempty_iff_ne_empty.2 fun h ↦ by simp [h] at hu₀
+  have hunorm : (u : Set E) ⊆ closedBall 0 (u.sup' hu (‖·‖) + 1) := by
+    simp only [subset_def, Finset.mem_coe, mem_closedBall, dist_zero_right, ← sub_le_iff_le_add,
+      Finset.le_sup'_iff]
+    exact fun x hx ↦ ⟨x, hx, by simp⟩
+  set ε' : ℝ := ε / 2 / (u.sup' hu (‖·‖) + 1)
+  have hε' : 0 < ε' := by
+    dsimp [ε']
+    obtain ⟨x, hx⟩ := id hu
+    have : 0 ≤ u.sup' hu (‖·‖) := Finset.le_sup'_of_le _ hx (norm_nonneg _)
+    positivity
+  set t : Finset E := ε' • u
+  have hε₀ : 0 < ε / 2 := by positivity
+  have htnorm : (t : Set E) ⊆ closedBall 0 (ε / 2) := by
+    simp [t, Set.set_smul_subset_iff₀ hε'.ne', hε₀.le, _root_.smul_closedBall, abs_of_nonneg hε'.le]
+    simpa [ε',  hε₀.ne'] using hunorm
+  refine ⟨t, ?_, ?_⟩
+  · simpa [t, interior_smul₀, ← convexHull_smul, zero_mem_smul_set_iff, hε'.ne']
+  calc
+    convexHull ℝ t ⊆ closedBall 0 (ε / 2) := convexHull_min htnorm (convex_closedBall ..)
+    _ ⊆ ball 0 ε := closedBall_subset_ball (by linarith)
+    _ ⊆ s := hεs

LeanCamCombi/Mathlib/Analysis/Convex/Segment.lean

@@ -0,0 +1,12 @@
+import Mathlib.Analysis.Convex.Segment
+import Mathlib.Topology.MetricSpace.PseudoMetric
+
+namespace Real
+variable {ε r : ℝ}
+
+open Metric
+
+lemma closedBall_eq_segment (hε : 0 ≤ ε) : closedBall r ε = segment ℝ (r - ε) (r + ε) := by
+  rw [closedBall_eq_Icc, segment_eq_Icc ((sub_le_self _ hε).trans $ le_add_of_nonneg_right hε)]
+
+end Real

LeanCamCombi/Mathlib/Analysis/Normed/Group/Basic.lean

@@ -0,0 +1,24 @@
+import Mathlib.Analysis.Normed.Group.Basic
+
+open scoped NNReal
+
+section ContinuousInv
+variable {α E : Type*} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : ℝ≥0}
+  {f : α → E} {s : Set α} {x : α}
+
+@[to_additive (attr := simp)]
+lemma lipschitzWith_inv_iff : LipschitzWith K f⁻¹ ↔ LipschitzWith K f := by simp [LipschitzWith]
+
+@[to_additive (attr := simp)]
+lemma lipschitzOnWith_inv_iff : LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s := by
+  simp [LipschitzOnWith]
+
+@[to_additive (attr := simp)]
+lemma locallyLipschitz_inv_iff : LocallyLipschitz f⁻¹ ↔ LocallyLipschitz f := by
+  simp [LocallyLipschitz]
+
+@[to_additive (attr := simp)]
+lemma antilipschitzWith_inv_iff : AntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f := by
+  simp [AntilipschitzWith]
+
+end ContinuousInv

LeanCamCombi/Mathlib/Topology/Algebra/Group/Basic.lean

@@ -0,0 +1,20 @@
+import Mathlib.Topology.Algebra.Group.Basic
+
+variable {α G : Type*}
+
+section ContinuousInv
+variable [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α]
+  {f : α → G} {s : Set α} {x : α}
+
+@[to_additive (attr := simp)]
+lemma continuous_inv_iff : Continuous f⁻¹ ↔ Continuous f := (Homeomorph.inv G).comp_continuous_iff
+
+@[to_additive (attr := simp)]
+lemma continuousAt_inv_iff : ContinuousAt f⁻¹ x ↔ ContinuousAt f x :=
+  (Homeomorph.inv G).comp_continuousAt_iff _ _
+
+@[to_additive (attr := simp)]
+lemma continuousOn_inv_iff : ContinuousOn f⁻¹ s ↔ ContinuousOn f s :=
+  (Homeomorph.inv G).comp_continuousOn_iff _ _
+
+end ContinuousInv