Skip to content

Commit 05a2cf5

Browse files
mans0954mans0954
committed
Merge branch 'master' into mans0954/Bilinear-SMulCommClass
2 parents eae5824 + 8ec1ec7 commit 05a2cf5

File tree

47 files changed

+1291
-580
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

47 files changed

+1291
-580
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -603,6 +603,7 @@ import Mathlib.Analysis.Calculus.MeanValue
603603
import Mathlib.Analysis.Calculus.Monotone
604604
import Mathlib.Analysis.Calculus.ParametricIntegral
605605
import Mathlib.Analysis.Calculus.ParametricIntervalIntegral
606+
import Mathlib.Analysis.Calculus.Rademacher
606607
import Mathlib.Analysis.Calculus.Series
607608
import Mathlib.Analysis.Calculus.TangentCone
608609
import Mathlib.Analysis.Calculus.Taylor

‎Mathlib/Algebra/Lie/Nilpotent.lean‎

Lines changed: 34 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -122,6 +122,7 @@ end LieSubmodule
122122

123123
namespace LieModule
124124

125+
variable {M₂ : Type w₁} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂]
125126
variable (R L M)
126127

127128
theorem antitone_lowerCentralSeries : Antitone <| lowerCentralSeries R L M := by
@@ -166,15 +167,23 @@ theorem iterate_toEndomorphism_mem_lowerCentralSeries₂ (x y : L) (m : M) (k :
166167

167168
variable {R L M}
168169

169-
theorem map_lowerCentralSeries_le {M₂ : Type w₁} [AddCommGroup M₂] [Module R M₂]
170-
[LieRingModule L M₂] [LieModule R L M₂] (k : ℕ) (f : M →ₗ⁅R,L⁆ M₂) :
171-
LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k := by
170+
theorem map_lowerCentralSeries_le (f : M →ₗ⁅R,L⁆ M₂) :
171+
(lowerCentralSeries R L M k).map f ≤ lowerCentralSeries R L M₂ k := by
172172
induction' k with k ih
173173
· simp only [Nat.zero_eq, lowerCentralSeries_zero, le_top]
174174
· simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
175175
exact LieSubmodule.mono_lie_right _ _ ⊤ ih
176176
#align lie_module.map_lower_central_series_le LieModule.map_lowerCentralSeries_le
177177

178+
lemma map_lowerCentralSeries_eq {f : M →ₗ⁅R,L⁆ M₂} (hf : Function.Surjective f) :
179+
(lowerCentralSeries R L M k).map f = lowerCentralSeries R L M₂ k := by
180+
apply le_antisymm (map_lowerCentralSeries_le k f)
181+
induction' k with k ih
182+
· rwa [lowerCentralSeries_zero, lowerCentralSeries_zero, top_le_iff, f.map_top, f.range_eq_top]
183+
· simp only [lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
184+
apply LieSubmodule.mono_lie_right
185+
assumption
186+
178187
variable (R L M)
179188

180189
open LieAlgebra
@@ -198,6 +207,12 @@ theorem exists_lowerCentralSeries_eq_bot_of_isNilpotent [IsNilpotent R L M] :
198207
∃ k, lowerCentralSeries R L M k = ⊥ :=
199208
IsNilpotent.nilpotent
200209

210+
@[simp] lemma iInf_lowerCentralSeries_eq_bot_of_isNilpotent [IsNilpotent R L M] :
211+
⨅ k, lowerCentralSeries R L M k = ⊥ := by
212+
obtain ⟨k, hk⟩ := exists_lowerCentralSeries_eq_bot_of_isNilpotent R L M
213+
rw [eq_bot_iff, ← hk]
214+
exact iInf_le _ _
215+
201216
/-- See also `LieModule.isNilpotent_iff_exists_ucs_eq_top`. -/
202217
theorem isNilpotent_iff : IsNilpotent R L M ↔ ∃ k, lowerCentralSeries R L M k = ⊥ :=
203218
⟨fun h => h.nilpotent, fun h => ⟨h⟩⟩
@@ -270,6 +285,18 @@ theorem nilpotentOfNilpotentQuotient {N : LieSubmodule R L M} (h₁ : N ≤ maxT
270285
exact map_lowerCentralSeries_le k (LieSubmodule.Quotient.mk' N)
271286
#align lie_module.nilpotent_of_nilpotent_quotient LieModule.nilpotentOfNilpotentQuotient
272287

288+
theorem isNilpotent_quotient_iff :
289+
IsNilpotent R L (M ⧸ N) ↔ ∃ k, lowerCentralSeries R L M k ≤ N := by
290+
rw [LieModule.isNilpotent_iff]
291+
refine exists_congr fun k ↦ ?_
292+
rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, map_lowerCentralSeries_eq k
293+
(LieSubmodule.Quotient.surjective_mk' N)]
294+
295+
theorem iInf_lcs_le_of_isNilpotent_quot (h : IsNilpotent R L (M ⧸ N)) :
296+
⨅ k, lowerCentralSeries R L M k ≤ N := by
297+
obtain ⟨k, hk⟩ := (isNilpotent_quotient_iff R L M N).mp h
298+
exact iInf_le_of_le k hk
299+
273300
/-- Given a nilpotent Lie module `M` with lower central series `M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥`, this is
274301
the natural number `k` (the number of inclusions).
275302
@@ -521,6 +548,10 @@ theorem LieModule.isNilpotent_of_top_iff :
521548
Equiv.lieModule_isNilpotent_iff LieSubalgebra.topEquiv (1 : M ≃ₗ[R] M) fun _ _ => rfl
522549
#align lie_module.is_nilpotent_of_top_iff LieModule.isNilpotent_of_top_iff
523550

551+
@[simp] lemma LieModule.isNilpotent_of_top_iff' :
552+
IsNilpotent R L {x // x ∈ (⊤ : LieSubmodule R L M)} ↔ IsNilpotent R L M :=
553+
Equiv.lieModule_isNilpotent_iff 1 (LinearEquiv.ofTop ⊤ rfl) fun _ _ ↦ rfl
554+
524555
end Morphisms
525556

526557
end NilpotentModules

‎Mathlib/Algebra/Lie/Quotient.lean‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -185,6 +185,15 @@ def mk' : M →ₗ⁅R,L⁆ M ⧸ N :=
185185
map_lie' := fun {_ _} => rfl }
186186
#align lie_submodule.quotient.mk' LieSubmodule.Quotient.mk'
187187

188+
@[simp]
189+
theorem surjective_mk' : Function.Surjective (mk' N) := surjective_quot_mk _
190+
191+
@[simp]
192+
theorem range_mk' : LieModuleHom.range (mk' N) = ⊤ := by simp [LieModuleHom.range_eq_top]
193+
194+
instance isNoetherian [IsNoetherian R M] : IsNoetherian R (M ⧸ N) :=
195+
Submodule.Quotient.isNoetherian (N : Submodule R M)
196+
188197
-- Porting note: LHS simplifies @[simp]
189198
theorem mk_eq_zero {m : M} : mk' N m = 0 ↔ m ∈ N :=
190199
Submodule.Quotient.mk_eq_zero N.toSubmodule
@@ -213,6 +222,10 @@ theorem lieModuleHom_ext ⦃f g : M ⧸ N →ₗ⁅R,L⁆ M⦄ (h : f.comp (mk'
213222
LieModuleHom.ext fun x => Quotient.inductionOn' x <| LieModuleHom.congr_fun h
214223
#align lie_submodule.quotient.lie_module_hom_ext LieSubmodule.Quotient.lieModuleHom_ext
215224

225+
lemma toEndomorphism_comp_mk' (x : L) :
226+
LieModule.toEndomorphism R L (M ⧸ N) x ∘ₗ mk' N = mk' N ∘ₗ LieModule.toEndomorphism R L M x :=
227+
rfl
228+
216229
end Quotient
217230

218231
end LieSubmodule

‎Mathlib/Algebra/Lie/Submodule.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1242,6 +1242,9 @@ theorem mem_range (n : N) : n ∈ f.range ↔ ∃ m, f m = n :=
12421242
theorem map_top : LieSubmodule.map f ⊤ = f.range := by ext; simp [LieSubmodule.mem_map]
12431243
#align lie_module_hom.map_top LieModuleHom.map_top
12441244

1245+
theorem range_eq_top : f.range = ⊤ ↔ Function.Surjective f := by
1246+
rw [SetLike.ext'_iff, coe_range, LieSubmodule.top_coe, Set.range_iff_surjective]
1247+
12451248
end LieModuleHom
12461249

12471250
namespace LieSubmodule

‎Mathlib/Algebra/Lie/Weights.lean‎

Lines changed: 135 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,15 @@ Copyright (c) 2021 Oliver Nash. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Oliver Nash
55
-/
6+
import Mathlib.Algebra.Ring.Divisibility.Lemmas
67
import Mathlib.Algebra.Lie.Nilpotent
78
import Mathlib.Algebra.Lie.TensorProduct
89
import Mathlib.Algebra.Lie.Character
910
import Mathlib.Algebra.Lie.Engel
1011
import Mathlib.Algebra.Lie.CartanSubalgebra
1112
import Mathlib.LinearAlgebra.Eigenspace.Basic
1213
import Mathlib.LinearAlgebra.TensorProduct.Tower
14+
import Mathlib.RingTheory.Artinian
1315

1416
#align_import algebra.lie.weights from "leanprover-community/mathlib"@"6b0169218d01f2837d79ea2784882009a0da1aa1"
1517

@@ -249,6 +251,139 @@ instance [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] :
249251
IsNilpotent R L (weightSpace M (0 : L → R)) :=
250252
isNilpotent_iff_forall'.mpr <| isNilpotent_toEndomorphism_weightSpace_zero M
251253

254+
variable (R L)
255+
256+
@[simp]
257+
lemma weightSpace_zero_normalizer_eq_self [LieAlgebra.IsNilpotent R L] :
258+
(weightSpace M (0 : L → R)).normalizer = weightSpace M 0 := by
259+
refine' le_antisymm _ (LieSubmodule.le_normalizer _)
260+
intro m hm
261+
rw [LieSubmodule.mem_normalizer] at hm
262+
simp only [mem_weightSpace, Pi.zero_apply, zero_smul, sub_zero] at hm ⊢
263+
intro y
264+
obtain ⟨k, hk⟩ := hm y y
265+
use k + 1
266+
simpa [pow_succ', LinearMap.mul_eq_comp]
267+
268+
lemma iSup_ucs_le_weightSpace_zero [LieAlgebra.IsNilpotent R L] :
269+
⨆ k, (⊥ : LieSubmodule R L M).ucs k ≤ weightSpace M (0 : L → R) := by
270+
simpa using LieSubmodule.ucs_le_of_normalizer_eq_self (weightSpace_zero_normalizer_eq_self R L M)
271+
272+
/-- See also `LieModule.iInf_lowerCentralSeries_eq_posFittingComp`. -/
273+
lemma iSup_ucs_eq_weightSpace_zero [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] :
274+
⨆ k, (⊥ : LieSubmodule R L M).ucs k = weightSpace M (0 : L → R) := by
275+
obtain ⟨k, hk⟩ := (LieSubmodule.isNilpotent_iff_exists_self_le_ucs
276+
<| weightSpace M (0 : L → R)).mp inferInstance
277+
refine le_antisymm (iSup_ucs_le_weightSpace_zero R L M) (le_trans hk ?_)
278+
exact le_iSup (fun k ↦ (⊥ : LieSubmodule R L M).ucs k) k
279+
280+
variable {L}
281+
282+
/-- If `M` is a representation of a nilpotent Lie algebra `L`, and `x : L`, then
283+
`posFittingCompOf R M x` is the infimum of the decreasing system
284+
`range φₓ ⊇ range φₓ² ⊇ range φₓ³ ⊇ ⋯` where `φₓ : End R M := toEndomorphism R L M x`. We call this
285+
the "positive Fitting component" because with appropriate assumptions (e.g., `R` is a field and
286+
`M` is finite-dimensional) `φₓ` induces the so-called Fitting decomposition: `M = M₀ ⊕ M₁` where
287+
`M₀ = weightSpaceOf M 0 x` and `M₁ = posFittingCompOf R M x`.
288+
289+
It is a Lie submodule because `L` is nilpotent. -/
290+
def posFittingCompOf [LieAlgebra.IsNilpotent R L] (x : L) : LieSubmodule R L M :=
291+
{ toSubmodule := ⨅ k, LinearMap.range (toEndomorphism R L M x ^ k)
292+
lie_mem := by
293+
set φ := toEndomorphism R L M x
294+
intros y m hm
295+
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
296+
Submodule.mem_toAddSubmonoid, Submodule.mem_iInf, LinearMap.mem_range] at hm ⊢
297+
intro k
298+
obtain ⟨N, hN⟩ := LieAlgebra.nilpotent_ad_of_nilpotent_algebra R L
299+
obtain ⟨m, rfl⟩ := hm (N + k)
300+
let f₁ : Module.End R (L ⊗[R] M) := (LieAlgebra.ad R L x).rTensor M
301+
let f₂ : Module.End R (L ⊗[R] M) := φ.lTensor L
302+
replace hN : f₁ ^ N = 0 := by ext; simp [hN]
303+
have h₁ : Commute f₁ f₂ := by ext; simp
304+
have h₂ : φ ∘ₗ toModuleHom R L M = toModuleHom R L M ∘ₗ (f₁ + f₂) := by ext; simp
305+
obtain ⟨q, hq⟩ := h₁.add_pow_dvd_pow_of_pow_eq_zero_right (N + k).le_succ hN
306+
use toModuleHom R L M (q (y ⊗ₜ m))
307+
change (φ ^ k).comp ((toModuleHom R L M : L ⊗[R] M →ₗ[R] M)) _ = _
308+
simp [LinearMap.commute_pow_left_of_commute h₂, LinearMap.comp_apply (g := (f₁ + f₂) ^ k),
309+
← LinearMap.comp_apply (g := q), ← LinearMap.mul_eq_comp, ← hq] }
310+
311+
variable {M} in
312+
lemma mem_posFittingCompOf [LieAlgebra.IsNilpotent R L] (x : L) (m : M) :
313+
m ∈ posFittingCompOf R M x ↔ ∀ (k : ℕ), ∃ n, (toEndomorphism R L M x ^ k) n = m := by
314+
simp [posFittingCompOf]
315+
316+
@[simp] lemma posFittingCompOf_le_lowerCentralSeries [LieAlgebra.IsNilpotent R L] (x : L) (k : ℕ) :
317+
posFittingCompOf R M x ≤ lowerCentralSeries R L M k := by
318+
suffices : ∀ m l, (toEndomorphism R L M x ^ l) m ∈ lowerCentralSeries R L M l
319+
· intro m hm
320+
obtain ⟨n, rfl⟩ := (mem_posFittingCompOf R x m).mp hm k
321+
exact this n k
322+
intro m l
323+
induction' l with l ih; simp
324+
simp only [lowerCentralSeries_succ, pow_succ, LinearMap.mul_apply]
325+
exact LieSubmodule.lie_mem_lie _ ⊤ (LieSubmodule.mem_top x) ih
326+
327+
@[simp] lemma posFittingCompOf_eq_bot_of_isNilpotent
328+
[LieAlgebra.IsNilpotent R L] [IsNilpotent R L M] (x : L) :
329+
posFittingCompOf R M x = ⊥ := by
330+
simp_rw [eq_bot_iff, ← iInf_lowerCentralSeries_eq_bot_of_isNilpotent, le_iInf_iff,
331+
posFittingCompOf_le_lowerCentralSeries, forall_const]
332+
333+
lemma exists_coe_posFittingCompOf_eq_of_isArtinian
334+
[LieAlgebra.IsNilpotent R L] [IsArtinian R M] (x : L) :
335+
∃ (k : ℕ), posFittingCompOf R M x = LinearMap.range (toEndomorphism R L M x ^ k) :=
336+
(toEndomorphism R L M x).exists_range_pow_eq_iInf
337+
338+
variable (L)
339+
340+
/-- If `M` is a representation of a nilpotent Lie algebra `L` with coefficients in `R`, then
341+
`posFittingComp R L M` is the span of the positive Fitting components of the action of `x` on `M`,
342+
as `x` ranges over `L`.
343+
344+
It is a Lie submodule because `L` is nilpotent. -/
345+
def posFittingComp [LieAlgebra.IsNilpotent R L] : LieSubmodule R L M :=
346+
⨆ x, posFittingCompOf R M x
347+
348+
lemma mem_posFittingComp [LieAlgebra.IsNilpotent R L] (m : M) :
349+
m ∈ posFittingComp R L M ↔ m ∈ ⨆ (x : L), posFittingCompOf R M x := by
350+
rfl
351+
352+
lemma posFittingCompOf_le_posFittingComp [LieAlgebra.IsNilpotent R L] (x : L) :
353+
posFittingCompOf R M x ≤ posFittingComp R L M := by
354+
rw [posFittingComp]; exact le_iSup (posFittingCompOf R M) x
355+
356+
lemma posFittingComp_le_iInf_lowerCentralSeries [LieAlgebra.IsNilpotent R L] :
357+
posFittingComp R L M ≤ ⨅ k, lowerCentralSeries R L M k := by
358+
simp [posFittingComp]
359+
360+
/-- See also `LieModule.iSup_ucs_eq_weightSpace_zero`. -/
361+
@[simp] lemma iInf_lowerCentralSeries_eq_posFittingComp
362+
[LieAlgebra.IsNilpotent R L] [IsNoetherian R M] [IsArtinian R M] :
363+
⨅ k, lowerCentralSeries R L M k = posFittingComp R L M := by
364+
refine le_antisymm ?_ (posFittingComp_le_iInf_lowerCentralSeries R L M)
365+
apply iInf_lcs_le_of_isNilpotent_quot
366+
rw [LieModule.isNilpotent_iff_forall']
367+
intro x
368+
obtain ⟨k, hk⟩ := exists_coe_posFittingCompOf_eq_of_isArtinian R M x
369+
use k
370+
ext ⟨m⟩
371+
set F := posFittingComp R L M
372+
replace hk : (toEndomorphism R L M x ^ k) m ∈ F := by
373+
apply posFittingCompOf_le_posFittingComp R L M x
374+
rw [← LieSubmodule.mem_coeSubmodule, hk]
375+
apply LinearMap.mem_range_self
376+
suffices (toEndomorphism R L (M ⧸ F) x ^ k) (LieSubmodule.Quotient.mk (N := F) m) =
377+
LieSubmodule.Quotient.mk (N := F) ((toEndomorphism R L M x ^ k) m) by simpa [this]
378+
have := LinearMap.congr_fun (LinearMap.commute_pow_left_of_commute
379+
(LieSubmodule.Quotient.toEndomorphism_comp_mk' F x) k) m
380+
simpa using this
381+
382+
@[simp] lemma posFittingComp_eq_bot_of_isNilpotent
383+
[LieAlgebra.IsNilpotent R L] [IsNilpotent R L M] :
384+
posFittingComp R L M = ⊥ := by
385+
simp [posFittingComp]
386+
252387
end LieModule
253388

254389
namespace LieAlgebra

‎Mathlib/Algebra/Order/Module.lean‎

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Frédéric Dupuis, Yaël Dillies
55
-/
66
import Mathlib.Algebra.Order.SMul
77

8-
#align_import algebra.order.module from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853"
8+
#align_import algebra.order.module from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
99

1010
/-!
1111
# Ordered module
@@ -217,6 +217,19 @@ theorem BddAbove.smul_of_nonpos (hc : c ≤ 0) (hs : BddAbove s) : BddBelow (c
217217

218218
end OrderedRing
219219

220+
section LinearOrderedRing
221+
variable [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k}
222+
223+
theorem smul_max_of_nonpos (ha : a ≤ 0) (b₁ b₂ : M) : a • max b₁ b₂ = min (a • b₁) (a • b₂) :=
224+
(antitone_smul_left ha : Antitone (_ : M → M)).map_max
225+
#align smul_max_of_nonpos smul_max_of_nonpos
226+
227+
theorem smul_min_of_nonpos (ha : a ≤ 0) (b₁ b₂ : M) : a • min b₁ b₂ = max (a • b₁) (a • b₂) :=
228+
(antitone_smul_left ha : Antitone (_ : M → M)).map_min
229+
#align smul_min_of_nonpos smul_min_of_nonpos
230+
231+
end LinearOrderedRing
232+
220233
section LinearOrderedField
221234

222235
variable [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M}

‎Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -334,16 +334,18 @@ end NeZero
334334
/-- A canonically linear-ordered additive monoid is a canonically ordered additive monoid
335335
whose ordering is a linear order. -/
336336
class CanonicallyLinearOrderedAddCommMonoid (α : Type*)
337-
extends CanonicallyOrderedAddCommMonoid α, LinearOrder α
337+
extends CanonicallyOrderedAddCommMonoid α, LinearOrderedAddCommMonoid α
338338
#align canonically_linear_ordered_add_monoid CanonicallyLinearOrderedAddCommMonoid
339339

340340
/-- A canonically linear-ordered monoid is a canonically ordered monoid
341341
whose ordering is a linear order. -/
342342
@[to_additive]
343-
class CanonicallyLinearOrderedCommMonoid (α : Type*) extends CanonicallyOrderedCommMonoid α,
344-
LinearOrder α
343+
class CanonicallyLinearOrderedCommMonoid (α : Type*)
344+
extends CanonicallyOrderedCommMonoid α, LinearOrderedCommMonoid α
345345
#align canonically_linear_ordered_monoid CanonicallyLinearOrderedCommMonoid
346346

347+
attribute [to_additive existing] CanonicallyLinearOrderedCommMonoid.toLinearOrderedCommMonoid
348+
347349
section CanonicallyLinearOrderedCommMonoid
348350

349351
variable [CanonicallyLinearOrderedCommMonoid α]

‎Mathlib/Algebra/Order/Monoid/Lemmas.lean‎

Lines changed: 22 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ import Mathlib.Init.Data.Ordering.Basic
99
import Mathlib.Order.MinMax
1010
import Mathlib.Tactic.Contrapose
1111

12-
#align_import algebra.order.monoid.lemmas from "leanprover-community/mathlib"@"2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c"
12+
#align_import algebra.order.monoid.lemmas from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
1313

1414
/-!
1515
# Ordered monoids
@@ -355,6 +355,27 @@ variable [LinearOrder α] {a b c d : α}
355355
#align min_le_max_of_add_le_add min_le_max_of_add_le_add
356356
#align min_le_max_of_mul_le_mul min_le_max_of_mul_le_mul
357357

358+
end LinearOrder
359+
360+
section LinearOrder
361+
variable [LinearOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
362+
[CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a b c d : α}
363+
364+
@[to_additive max_add_add_le_max_add_max]
365+
theorem max_mul_mul_le_max_mul_max' : max (a * b) (c * d) ≤ max a c * max b d :=
366+
max_le (mul_le_mul' (le_max_left _ _) <| le_max_left _ _) <|
367+
mul_le_mul' (le_max_right _ _) <| le_max_right _ _
368+
#align max_mul_mul_le_max_mul_max' max_mul_mul_le_max_mul_max'
369+
#align max_add_add_le_max_add_max max_add_add_le_max_add_max
370+
371+
--TODO: Also missing `min_mul_min_le_min_mul_mul`
372+
@[to_additive min_add_min_le_min_add_add]
373+
theorem min_mul_min_le_min_mul_mul' : min a c * min b d ≤ min (a * b) (c * d) :=
374+
le_min (mul_le_mul' (min_le_left _ _) <| min_le_left _ _) <|
375+
mul_le_mul' (min_le_right _ _) <| min_le_right _ _
376+
#align min_mul_min_le_min_mul_mul' min_mul_min_le_min_mul_mul'
377+
#align min_add_min_le_min_add_add min_add_min_le_min_add_add
378+
358379
end LinearOrder
359380
end Mul
360381

0 commit comments

Comments
 (0)