Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
9973e93
convex_of_nonneg_algebraMap and convex_of_nonneg_surjective_algebraMap
mans0954 Sep 2, 2025
08dbb29
convex_ordered_ring_of_convex_ordered_algebra
mans0954 Sep 2, 2025
6687f3c
convex_RCLike_iff_convex_real
mans0954 Sep 2, 2025
eb4d69d
Tweak
mans0954 Sep 2, 2025
7382b77
Merge branch 'master' into convex-algebramap
mans0954 Sep 2, 2025
4df95f0
AbsConvex
mans0954 Sep 4, 2025
7b8daf9
AbsConvexOpen pt 1
mans0954 Sep 4, 2025
9ac32db
Merge branch 'convex-algebramap' into absconvex-refactor
mans0954 Sep 4, 2025
4a9fa8d
AbsConvexOpen pt
mans0954 Sep 4, 2025
46bd997
Use RCLike in polar_AbsConvex
mans0954 Sep 4, 2025
8beabf1
Merge branch 'master' into convex-algebramap
mans0954 Sep 4, 2025
81a62b4
docstring
mans0954 Sep 5, 2025
7de88bc
Merge branch 'master' into absconvex-refactor
mans0954 Sep 5, 2025
55655b8
docstring
mans0954 Sep 5, 2025
ec0d1ec
Avoid large import
mans0954 Sep 6, 2025
364684d
Revert the additional complexity added in #21002 which is no longer n…
mans0954 Sep 6, 2025
d9ba861
Use SMulPosMono instead
mans0954 Sep 7, 2025
60f060a
Merge branch 'master' into convex-algebramap
mans0954 Sep 7, 2025
8fa8d1d
Merge branch 'convex-algebramap' into absconvex-refactor
mans0954 Sep 7, 2025
d4809e2
Fix
mans0954 Sep 7, 2025
5532acc
Merge branch 'master' into absconvex-refactor
mans0954 Sep 30, 2025
19e2755
Merge branch 'master' into absconvex-refactor
mans0954 Oct 2, 2025
f8d80dc
Fix
mans0954 Oct 2, 2025
de89d3a
Merge branch 'master' into absconvex-refactor
mans0954 Oct 3, 2025
bcd8225
Merge branch 'master' into absconvex-refactor
mans0954 Oct 3, 2025
43d3e4b
Indent
mans0954 Oct 3, 2025
409fc83
Remove commented out import
mans0954 Oct 3, 2025
13d03fd
Remove commented out lines
mans0954 Oct 3, 2025
d04451f
scope ComplexOrder
mans0954 Oct 6, 2025
f0e67ae
Merge branch 'master' into absconvex-refactor
mans0954 Oct 9, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 8 additions & 12 deletions Mathlib/Analysis/Convex/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -172,17 +172,13 @@ theorem Convex.is_linear_image (hs : Convex π•œ s) {f : E β†’ F} (hf : IsLinear
Convex π•œ (f '' s) :=
hs.linear_image <| hf.mk' f

theorem Convex.linear_preimage {π•œβ‚ : Type*} [Semiring π•œβ‚] [Module π•œβ‚ E] [Module π•œβ‚ F] {s : Set F}
[SMul π•œ π•œβ‚] [IsScalarTower π•œ π•œβ‚ E] [IsScalarTower π•œ π•œβ‚ F] (hs : Convex π•œ s) (f : E β†’β‚—[π•œβ‚] F) :
Convex π•œ (f ⁻¹' s) := fun x hx y hy a b ha hb hab => by
rw [mem_preimage, f.map_add, LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower]
exact hs hx hy ha hb hab

theorem Convex.is_linear_preimage {π•œβ‚ : Type*} [Semiring π•œβ‚] [Module π•œβ‚ E] [Module π•œβ‚ F] {s : Set F}
[SMul π•œ π•œβ‚] [IsScalarTower π•œ π•œβ‚ E] [IsScalarTower π•œ π•œβ‚ F] (hs : Convex π•œ s) {f : E β†’ F}
(hf : IsLinearMap π•œβ‚ f) :
Convex π•œ (f ⁻¹' s) :=
hs.linear_preimage <| hf.mk' f
theorem Convex.linear_preimage {s : Set F} (hs : Convex π•œ s) (f : E β†’β‚—[π•œ] F) : Convex π•œ (f ⁻¹' s) :=
fun x hx y hy a b ha hb hab => by
rw [mem_preimage, f.map_add, LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower]
exact hs hx hy ha hb hab

theorem Convex.is_linear_preimage {s : Set F} (hs : Convex π•œ s) {f : E β†’ F} (hf : IsLinearMap π•œ f) :
Convex π•œ (f ⁻¹' s) := hs.linear_preimage <| hf.mk' f

theorem Convex.add {t : Set E} (hs : Convex π•œ s) (ht : Convex π•œ t) : Convex π•œ (s + t) := by
rw [← add_image_prod]
Expand Down Expand Up @@ -455,7 +451,7 @@ theorem Convex.affine_image (f : E →ᡃ[π•œ] F) (hs : Convex π•œ s) : Convex
exact (hs hx).affine_image _

theorem Convex.neg (hs : Convex π•œ s) : Convex π•œ (-s) :=
hs.is_linear_preimage IsLinearMap.isLinearMap_neg (π•œβ‚ := π•œ)
hs.is_linear_preimage IsLinearMap.isLinearMap_neg

theorem Convex.sub (hs : Convex π•œ s) (ht : Convex π•œ t) : Convex π•œ (s - t) := by
rw [sub_eq_add_neg]
Expand Down
60 changes: 24 additions & 36 deletions Mathlib/Analysis/LocallyConvex/AbsConvex.lean
Original file line number Diff line number Diff line change
Expand Up @@ -30,14 +30,6 @@ topological vector space has a basis consisting of absolutely convex sets.
* `closedAbsConvexHull_closure_eq_closedAbsConvexHull` : the closed absolutely convex hull of the
closure of `s` equals the closed absolutely convex hull of `s`;

## Implementation notes

Mathlib's definition of `Convex` requires the scalars to be an `OrderedSemiring` whereas the
definition of `Balanced` requires the scalars to be a `SeminormedRing`. Mathlib doesn't currently
have a concept of a semi-normed ordered ring, so we define a set as `AbsConvex` if it is balanced
over a `SeminormedRing` `π•œ` and convex over `ℝ`, assuming `IsScalarTower ℝ π•œ E` and
`SMulCommClass ℝ π•œ E` where required.

## Tags

disks, convex, balanced
Expand All @@ -51,13 +43,10 @@ variable {π•œ E : Type*}

section AbsolutelyConvex

variable (π•œ) [SeminormedRing π•œ] [SMul π•œ E] [SMul ℝ E] [AddCommMonoid E]
/-- A set is absolutely convex if it is balanced and convex. Mathlib's definition of `Convex`
requires the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` requires the
scalars to be a `SeminormedRing`. Mathlib doesn't currently have a concept of a semi-normed ordered
ring, so we define a set as `AbsConvex` if it is balanced over a `SeminormedRing` `π•œ` and convex
over `ℝ`. -/
def AbsConvex (s : Set E) : Prop := Balanced π•œ s ∧ Convex ℝ s
variable (π•œ) [SeminormedRing π•œ] [SMul π•œ E] [AddCommMonoid E] [PartialOrder π•œ]

/-- A set is absolutely convex if it is balanced and convex. -/
def AbsConvex (s : Set E) : Prop := Balanced π•œ s ∧ Convex π•œ s

variable {π•œ}

Expand Down Expand Up @@ -97,7 +86,7 @@ theorem absConvex_absConvexHull : AbsConvex π•œ (absConvexHull π•œ s) :=
theorem balanced_absConvexHull : Balanced π•œ (absConvexHull π•œ s) :=
absConvex_absConvexHull.1

theorem convex_absConvexHull : Convex ℝ (absConvexHull π•œ s) :=
theorem convex_absConvexHull : Convex π•œ (absConvexHull π•œ s) :=
absConvex_absConvexHull.2

variable (π•œ s) in
Expand Down Expand Up @@ -193,9 +182,9 @@ end AbsolutelyConvex

section NormedField

variable [NormedField π•œ]
[AddCommGroup E] [Module ℝ E] [Module π•œ E] [TopologicalSpace E]
[IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [ContinuousSMul π•œ E]
variable [NormedField π•œ] [PartialOrder π•œ]
[AddCommGroup E] [Module π•œ E] [TopologicalSpace E]
[IsTopologicalAddGroup E] [ContinuousSMul π•œ E]

theorem AbsConvex.closure {s : Set E} (hs : AbsConvex π•œ s) : AbsConvex π•œ (closure s) :=
⟨Balanced.closure hs.1, Convex.closure hs.2⟩
Expand All @@ -211,23 +200,22 @@ end NormedField
section NontriviallyNormedField

variable (π•œ E)
variable [NontriviallyNormedField π•œ] [AddCommGroup E] [Module π•œ E]
variable [Module ℝ E] [SMulCommClass ℝ π•œ E]
variable [TopologicalSpace E] [LocallyConvexSpace ℝ E] [ContinuousSMul π•œ E]
variable [NontriviallyNormedField π•œ] [PartialOrder π•œ] [AddCommGroup E] [Module π•œ E]
variable [TopologicalSpace E] [LocallyConvexSpace π•œ E] [ContinuousSMul π•œ E]

theorem nhds_hasBasis_absConvex :
(𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ 𝓝 (0 : E) ∧ AbsConvex π•œ s) id := by
refine
(LocallyConvexSpace.convex_basis_zero ℝ E).to_hasBasis (fun s hs => ?_) fun s hs =>
(LocallyConvexSpace.convex_basis_zero π•œ E).to_hasBasis (fun s hs => ?_) fun s hs =>
⟨s, ⟨hs.1, hs.2.2⟩, rfl.subset⟩
refine ⟨convexHull ℝ (balancedCore π•œ s), ?_, convexHull_min (balancedCore_subset s) hs.2⟩
refine ⟨Filter.mem_of_superset (balancedCore_mem_nhds_zero hs.1) (subset_convexHull ℝ _), ?_⟩
refine ⟨convexHull π•œ (balancedCore π•œ s), ?_, convexHull_min (balancedCore_subset s) hs.2⟩
refine ⟨Filter.mem_of_superset (balancedCore_mem_nhds_zero hs.1) (subset_convexHull π•œ _), ?_⟩
refine ⟨(balancedCore_balanced s).convexHull, ?_⟩
exact convex_convexHull ℝ (balancedCore π•œ s)
exact convex_convexHull π•œ (balancedCore π•œ s)

variable [ContinuousSMul ℝ E] [IsTopologicalAddGroup E]
variable [IsTopologicalAddGroup E]

theorem nhds_hasBasis_absConvex_open :
theorem nhds_hasBasis_absConvex_open [ZeroLEOneClass π•œ] :
(𝓝 (0 : E)).HasBasis (fun s => (0 : E) ∈ s ∧ IsOpen s ∧ AbsConvex π•œ s) id := by
refine (nhds_hasBasis_absConvex π•œ E).to_hasBasis ?_ ?_
· rintro s ⟨hs_nhds, hs_balanced, hs_convex⟩
Expand All @@ -242,26 +230,26 @@ end NontriviallyNormedField

section

variable (π•œ) [NontriviallyNormedField π•œ]
variable [AddCommGroup E] [Module ℝ E] [Module π•œ E]
variable (π•œ) [NontriviallyNormedField π•œ] [PartialOrder π•œ]
variable [AddCommGroup E] [Module π•œ E]

theorem absConvexHull_add_subset {s t : Set E} :
absConvexHull π•œ (s + t) βŠ† absConvexHull π•œ s + absConvexHull π•œ t :=
absConvexHull_min (add_subset_add subset_absConvexHull subset_absConvexHull)
⟨Balanced.add balanced_absConvexHull balanced_absConvexHull,
Convex.add convex_absConvexHull convex_absConvexHull⟩

theorem absConvexHull_eq_convexHull_balancedHull [SMulCommClass ℝ π•œ E] {s : Set E} :
absConvexHull π•œ s = convexHull ℝ (balancedHull π•œ s) := le_antisymm
theorem absConvexHull_eq_convexHull_balancedHull {s : Set E} :
absConvexHull π•œ s = convexHull π•œ (balancedHull π•œ s) := le_antisymm
(absConvexHull_min
((subset_convexHull ℝ s).trans (convexHull_mono (subset_balancedHull π•œ)))
((subset_convexHull π•œ s).trans (convexHull_mono (subset_balancedHull π•œ)))
⟨Balanced.convexHull (balancedHull.balanced s), convex_convexHull ..⟩)
(convexHull_min (balanced_absConvexHull.balancedHull_subset_of_subset subset_absConvexHull)
convex_absConvexHull)

/-- In general, equality doesn't hold here - e.g. consider `s := {(-1, 1), (1, 1)}` in `ℝ²`. -/
theorem balancedHull_convexHull_subseteq_absConvexHull {s : Set E} :
balancedHull π•œ (convexHull ℝ s) βŠ† absConvexHull π•œ s :=
balancedHull π•œ (convexHull π•œ s) βŠ† absConvexHull π•œ s :=
balanced_absConvexHull.balancedHull_subset_of_subset
(convexHull_min subset_absConvexHull convex_absConvexHull)

Expand Down Expand Up @@ -294,7 +282,7 @@ theorem convexHull_union_neg_eq_absConvexHull {s : Set E} :
exact convexHull_mono balancedHull_subset_convexHull_union_neg)

variable (E π•œ) {s : Set E}
variable [NontriviallyNormedField π•œ] [Module π•œ E] [SMulCommClass ℝ π•œ E]
variable [NontriviallyNormedField π•œ] [PartialOrder π•œ] [Module π•œ E] [SMulCommClass ℝ π•œ E]
variable [UniformSpace E] [IsUniformAddGroup E] [lcs : LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E]

-- TVS II.25 Prop3
Expand All @@ -307,7 +295,7 @@ theorem totallyBounded_absConvexHull (hs : TotallyBounded s) :

end

lemma zero_mem_absConvexHull {s : Set E} [SeminormedRing π•œ] [AddCommGroup E] [Module ℝ E]
lemma zero_mem_absConvexHull {s : Set E} [SeminormedRing π•œ] [PartialOrder π•œ] [AddCommGroup E]
[Module π•œ E] [Nonempty s] : 0 ∈ absConvexHull π•œ s :=
balanced_absConvexHull.zero_mem (Nonempty.mono subset_absConvexHull Set.Nonempty.of_subtype)

Expand Down
17 changes: 10 additions & 7 deletions Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,8 @@ variable {π•œ E : Type*}
section AbsolutelyConvexSets

variable [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing π•œ]
variable [SMul π•œ E] [SMul ℝ E]
variable (π•œ E)
variable [SMul π•œ E]
variable (π•œ E) [PartialOrder π•œ]

/-- The type of absolutely convex open sets. -/
def AbsConvexOpenSets :=
Expand All @@ -63,7 +63,7 @@ theorem coe_nhds (s : AbsConvexOpenSets π•œ E) : (s : Set E) ∈ 𝓝 (0 : E) :
theorem coe_balanced (s : AbsConvexOpenSets π•œ E) : Balanced π•œ (s : Set E) :=
s.2.2.2.1

theorem coe_convex (s : AbsConvexOpenSets π•œ E) : Convex ℝ (s : Set E) :=
theorem coe_convex (s : AbsConvexOpenSets π•œ E) : Convex π•œ (s : Set E) :=
s.2.2.2.2

end AbsConvexOpenSets
Expand All @@ -82,9 +82,11 @@ variable [Module π•œ E] [Module ℝ E] [IsScalarTower ℝ π•œ E]
variable [ContinuousSMul ℝ E]
variable (π•œ E)

open scoped ComplexOrder

/-- The family of seminorms defined by the gauges of absolute convex open sets. -/
noncomputable def gaugeSeminormFamily : SeminormFamily π•œ E (AbsConvexOpenSets π•œ E) := fun s =>
gaugeSeminorm s.coe_balanced s.coe_convex (absorbent_nhds_zero s.coe_nhds)
gaugeSeminorm s.coe_balanced (s.coe_convex.lift ℝ) (absorbent_nhds_zero s.coe_nhds)

variable {π•œ E}

Expand All @@ -93,10 +95,10 @@ theorem gaugeSeminormFamily_ball (s : AbsConvexOpenSets π•œ E) :
dsimp only [gaugeSeminormFamily]
rw [Seminorm.ball_zero_eq]
simp_rw [gaugeSeminorm_toFun]
exact gauge_lt_one_eq_self_of_isOpen s.coe_convex s.coe_zero_mem s.coe_isOpen
exact gauge_lt_one_eq_self_of_isOpen (s.coe_convex.lift ℝ) s.coe_zero_mem s.coe_isOpen

variable [IsTopologicalAddGroup E] [ContinuousSMul π•œ E]
variable [SMulCommClass ℝ π•œ E] [LocallyConvexSpace ℝ E]
variable [LocallyConvexSpace π•œ E]

/-- The topology of a locally convex space is induced by the gauge seminorm family. -/
theorem with_gaugeSeminormFamily : WithSeminorms (gaugeSeminormFamily π•œ E) := by
Expand All @@ -114,7 +116,8 @@ theorem with_gaugeSeminormFamily : WithSeminorms (gaugeSeminormFamily π•œ E) :=
⟨mem_iInterβ‚‚.mpr fun _ _ => by simp [hr],
isOpen_biInter_finset fun S _ => ?_,
balanced_iInterβ‚‚ fun _ _ => Seminorm.balanced_ball_zero _ _,
convex_iInterβ‚‚ fun _ _ => Seminorm.convex_ball ..⟩
convex_iInterβ‚‚ fun _ _ => (convex_of_nonneg_surjective_algebraMap _
(fun _ => RCLike.nonneg_iff_exists_ofReal.mp) (Seminorm.convex_ball _ _ _) ..)⟩
-- The only nontrivial part is to show that the ball is open
have hr' : r = β€–(r : π•œ)β€– * 1 := by simp [abs_of_pos hr]
have hr'' : (r : π•œ) β‰  0 := by simp [hr.ne']
Expand Down
14 changes: 6 additions & 8 deletions Mathlib/Analysis/LocallyConvex/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -265,18 +265,16 @@ end NormedField

section NontriviallyNormedField

variable [NontriviallyNormedField π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E}
variable [NontriviallyNormedField π•œ] [PartialOrder π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E}

variable [Module ℝ E] [SMulCommClass ℝ π•œ E]

protected theorem Balanced.convexHull (hs : Balanced π•œ s) : Balanced π•œ (convexHull ℝ s) := by
suffices Convex ℝ { x | βˆ€ a : π•œ, β€–aβ€– ≀ 1 β†’ a β€’ x ∈ convexHull ℝ s } by
protected theorem Balanced.convexHull (hs : Balanced π•œ s) : Balanced π•œ (convexHull π•œ s) := by
suffices Convex π•œ { x | βˆ€ a : π•œ, β€–aβ€– ≀ 1 β†’ a β€’ x ∈ convexHull π•œ s } by
rw [balanced_iff_smul_mem] at hs ⊒
refine fun a ha x hx => convexHull_min ?_ this hx a ha
exact fun y hy a ha => subset_convexHull ℝ s (hs ha hy)
exact fun y hy a ha => subset_convexHull π•œ s (hs ha hy)
intro x hx y hy u v hu hv huv a ha
simp only [smul_add, ← smul_comm]
exact convex_convexHull ℝ s (hx a ha) (hy a ha) hu hv huv
rw [smul_add, ← smul_comm u, ← smul_comm v]
exact convex_convexHull π•œ s (hx a ha) (hy a ha) hu hv huv

end NontriviallyNormedField

Expand Down
7 changes: 3 additions & 4 deletions Mathlib/Analysis/Normed/Module/Dual.lean
Original file line number Diff line number Diff line change
Expand Up @@ -236,18 +236,17 @@ namespace LinearMap
section NormedField

variable {π•œ E F : Type*}
variable [NormedField π•œ] [NormedSpace ℝ π•œ] [AddCommMonoid E] [AddCommMonoid F]
variable [RCLike π•œ] [AddCommMonoid E] [AddCommMonoid F]
variable [Module π•œ E] [Module π•œ F]

variable {B : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ} (s : Set E)

variable [Module ℝ F] [IsScalarTower ℝ π•œ F] [IsScalarTower ℝ π•œ π•œ]

open ComplexOrder in
theorem polar_AbsConvex : AbsConvex π•œ (B.polar s) := by
rw [polar_eq_biInter_preimage]
exact AbsConvex.iInterβ‚‚ fun i hi =>
⟨balanced_closedBall_zero.mulActionHom_preimage (f := (B i : (F β†’β‚‘[(RingHom.id π•œ)] π•œ))),
(convex_closedBall _ _).linear_preimage (B i)⟩
(convex_RCLike_iff_convex_real.mpr (convex_closedBall 0 1)).linear_preimage _⟩

end NormedField

Expand Down