Skip to content

Commit

Permalink
Bump mathlib
Browse files Browse the repository at this point in the history
  • Loading branch information
YaelDillies committed Jan 3, 2024
1 parent a30cfb8 commit cad35ac
Show file tree
Hide file tree
Showing 5 changed files with 10 additions and 57 deletions.
2 changes: 1 addition & 1 deletion LeanAPAP.lean
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,9 @@ import LeanAPAP.Mathlib.Algebra.DirectSum.Basic
import LeanAPAP.Mathlib.Algebra.Function.Support
import LeanAPAP.Mathlib.Algebra.Group.Basic
import LeanAPAP.Mathlib.Algebra.Group.Equiv.Basic
import LeanAPAP.Mathlib.Algebra.Group.TypeTags
import LeanAPAP.Mathlib.Algebra.GroupPower.Basic
import LeanAPAP.Mathlib.Algebra.GroupPower.Order
import LeanAPAP.Mathlib.Algebra.Group.TypeTags
import LeanAPAP.Mathlib.Algebra.GroupWithZero.Units.Lemmas
import LeanAPAP.Mathlib.Algebra.ModEq
import LeanAPAP.Mathlib.Algebra.Module.Basic
Expand Down
47 changes: 0 additions & 47 deletions LeanAPAP/Mathlib/Algebra/BigOperators/Order.lean
Original file line number Diff line number Diff line change
Expand Up @@ -44,50 +44,3 @@ example (a : ℕ → ℤ) : 0 < ∑ j in ({1} : Finset ℕ), (a j^2 + 1) := by
positivity

end Mathlib.Meta.Positivity

namespace Finset

open Function
open scoped BigOperators

variable {ι N : Type*} [OrderedCommMonoid N] {f g : ι → N} {s t : Finset ι}

@[to_additive sum_eq_zero_iff_of_nonpos]
lemma prod_eq_one_iff_of_le_one'' : (∀ i ∈ s, f i ≤ 1) → ((∏ i in s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) :=
@prod_eq_one_iff_of_one_le' _ Nᵒᵈ _ _ _

end Finset

namespace Fintype
variable {ι α : Type*} [OrderedCommMonoid α] [Fintype ι] {f : ι → α}

-- TODO: Replace `Fintype.prod_eq_one_iff_of_one_le`
@[to_additive]
lemma prod_eq_one_iff_of_one_le' (hf : 1 ≤ f) : ∏ i, f i = 1 ↔ f = 1 :=
(Finset.prod_eq_one_iff_of_one_le' fun i _ ↦ hf i).trans $ by simp [Function.funext_iff]

-- TODO: Replace `Fintype.prod_eq_one_iff_of_le_one`
@[to_additive]
lemma prod_eq_one_iff_of_le_one' (hf : f ≤ 1) : ∏ i, f i = 1 ↔ f = 1 :=
(Finset.prod_eq_one_iff_of_le_one'' fun i _ ↦ hf i).trans $ by simp [Function.funext_iff]

end Fintype

namespace Finset
variable {α 𝕜 : Type*} [LinearOrderedCommRing 𝕜]

lemma sum_mul_sq_le_sq_mul_sq (s : Finset α) (f g : α → 𝕜) :
(∑ i in s, f i * g i) ^ 2 ≤ (∑ i in s, f i ^ 2) * ∑ i in s, g i ^ 2 := by
have h : 0 ≤ ∑ i in s, (f i * ∑ j in s, g j ^ 2 - g i * ∑ j in s, f j * g j) ^ 2 := by positivity
simp_rw [sub_sq, sum_add_distrib, Finset.sum_sub_distrib, mul_pow, mul_assoc, ←mul_sum, ←
sum_mul, mul_left_comm, ←mul_assoc, ←sum_mul, mul_right_comm, ←sq, mul_comm, sub_add,
two_mul, add_sub_cancel, sq (∑ j in s, g j ^ 2), ←mul_assoc, ←mul_sub_right_distrib] at h
obtain h' | h' := (sum_nonneg fun i _ ↦ sq_nonneg (g i)).eq_or_lt
· have h'' : ∀ i ∈ s, g i = 0 := fun i hi ↦ by
simpa using (sum_eq_zero_iff_of_nonneg fun i _ ↦ sq_nonneg (g i)).1 h'.symm i hi
rw [←h', sum_congr rfl (show ∀ i ∈ s, f i * g i = 0 from fun i hi ↦ by simp [h'' i hi])]
simp
· rw [←sub_nonneg]
exact nonneg_of_mul_nonneg_left h h'

end Finset
10 changes: 5 additions & 5 deletions LeanAPAP/Mathlib/Data/Real/ConjugateExponents.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ Change everything to using `x⁻¹` instead of `1 / x`.

open scoped ENNReal

attribute [mk_iff Real.isConjugateExponent_iff'] Real.IsConjugateExponent

namespace Real.IsConjugateExponent
variable {p q : ℝ} (h : p.IsConjugateExponent q)

attribute [mk_iff] IsConjugateExponent

lemma inv_add_inv_conj' : p⁻¹ + q⁻¹ = 1 := by simpa only [one_div] using h.inv_add_inv_conj

lemma one_sub_inv : 1 - p⁻¹ = q⁻¹ := sub_eq_of_eq_add' h.inv_add_inv_conj'.symm
Expand Down Expand Up @@ -43,11 +43,11 @@ variable {a b p q : ℝ≥0} (h : p.IsConjExponent q)

@[simp, norm_cast]
lemma isConjugateExponent_coe : (p : ℝ).IsConjugateExponent q ↔ p.IsConjExponent q := by
simp [Real.IsConjugateExponent_iff, IsConjExponent_iff]; norm_cast
simp [Real.isConjugateExponent_iff', isConjExponent_iff]; norm_cast

alias ⟨_, IsConjExponent.coe⟩ := isConjugateExponent_coe

lemma isConjExponent_iff (h : 1 < p) : p.IsConjExponent q ↔ q = p / (p - 1) := by
lemma isConjExponent_iff' (h : 1 < p) : p.IsConjExponent q ↔ q = p / (p - 1) := by
rw [← isConjugateExponent_coe, Real.isConjugateExponent_iff (mod_cast h), ← NNReal.coe_eq,
NNReal.coe_div, NNReal.coe_sub h.le, NNReal.coe_one]

Expand All @@ -70,7 +70,7 @@ lemma inv_ne_zero : p⁻¹ ≠ 0 := h.inv_pos.ne'
lemma one_sub_inv : 1 - p⁻¹ = q⁻¹ := tsub_eq_of_eq_add_rev h.inv_add_inv_conj.symm

protected lemma conjExponent (h : 1 < p) : p.IsConjExponent (conjExponent p) :=
(isConjExponent_iff h).2 rfl
(isConjExponent_iff' h).2 rfl

lemma conj_eq : q = p / (p - 1) := by
simpa only [← NNReal.coe_one, ← NNReal.coe_sub h.one_le, ← NNReal.coe_div, NNReal.coe_eq]
Expand Down
4 changes: 2 additions & 2 deletions LeanAPAP/Prereqs/Expect/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -467,10 +467,10 @@ section OrderedAddCommMonoid
variable [OrderedAddCommMonoid α] [Module ℚ≥0 α] {f : ι → α}

lemma expect_eq_zero_iff_of_nonneg [Nonempty ι] (hf : 0 ≤ f) : 𝔼 i, f i = 0 ↔ f = 0 := by
simp [expect, sum_eq_zero_iff_of_nonneg' hf, univ_nonempty.ne_empty]
simp [expect, sum_eq_zero_iff_of_nonneg hf, univ_nonempty.ne_empty]

lemma expect_eq_zero_iff_of_nonpos [Nonempty ι] (hf : f ≤ 0) : 𝔼 i, f i = 0 ↔ f = 0 := by
simp [expect, sum_eq_zero_iff_of_nonpos' hf, univ_nonempty.ne_empty]
simp [expect, sum_eq_zero_iff_of_nonpos hf, univ_nonempty.ne_empty]

end OrderedAddCommMonoid
end Fintype
Expand Down
4 changes: 2 additions & 2 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"rev": "e04a464df1da4a130b5fa9aaff1dcf79d92d3888",
"rev": "7d58fa3955c424de04895b4379b4c21d2eb97501",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": null,
Expand Down Expand Up @@ -85,7 +85,7 @@
{"url": "https://github.com/leanprover/doc-gen4",
"type": "git",
"subDir": null,
"rev": "86d5c219a9ad7aa686c9e0e704af030e203c63a1",
"rev": "eab9173b56295c3dadf46e104ab342060cbe2af8",
"name": "«doc-gen4»",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand Down

0 comments on commit cad35ac

Please sign in to comment.