diff --git a/LeanAPAP.lean b/LeanAPAP.lean index c1dc7abf71..efb7e390b1 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -1,13 +1,10 @@ import LeanAPAP.Extras.BSG import LeanAPAP.FiniteField import LeanAPAP.Integer -import LeanAPAP.Mathlib.Algebra.BigOperators.Group.Finset import LeanAPAP.Mathlib.Algebra.Group.AddChar import LeanAPAP.Mathlib.Algebra.Group.Basic import LeanAPAP.Mathlib.Algebra.Group.Pointwise.Finset import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic -import LeanAPAP.Mathlib.Algebra.Order.BigOperators.Group.Finset -import LeanAPAP.Mathlib.Algebra.Order.Field.Defs import LeanAPAP.Mathlib.Algebra.Order.Floor import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled diff --git a/LeanAPAP/FiniteField.lean b/LeanAPAP/FiniteField.lean index a3865701ab..0e0a9daaf7 100644 --- a/LeanAPAP/FiniteField.lean +++ b/LeanAPAP/FiniteField.lean @@ -1,5 +1,4 @@ import Mathlib.FieldTheory.Finite.Basic -import LeanAPAP.Mathlib.Algebra.Order.BigOperators.Group.Finset import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic import LeanAPAP.Mathlib.Algebra.Order.Ring.Cast diff --git a/LeanAPAP/Mathlib/Algebra/BigOperators/Group/Finset.lean b/LeanAPAP/Mathlib/Algebra/BigOperators/Group/Finset.lean deleted file mode 100644 index 622e47e6a9..0000000000 --- a/LeanAPAP/Mathlib/Algebra/BigOperators/Group/Finset.lean +++ /dev/null @@ -1,10 +0,0 @@ -import Mathlib.Algebra.BigOperators.Group.Finset - -namespace Fintype -variable {ι α : Type*} [Fintype ι] [CommMonoid α] [DecidableEq ι] - -@[to_additive] -lemma prod_ite_mem (s : Finset ι) (f : ι → α) : ∏ i, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i := by - simp - -end Fintype diff --git a/LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean b/LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean index 90f2073173..dca272e63f 100644 --- a/LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean +++ b/LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean @@ -4,9 +4,8 @@ import Mathlib.Data.Finset.Density open scoped Pointwise namespace Finset -variable {α β : Type*} [Group α] [Fintype β] [DecidableEq β] [MulAction α β] +variable {α : Type*} [DecidableEq α] [InvolutiveInv α] [Fintype α] -@[to_additive (attr := simp)] -lemma dens_smul_finset (a : α) (s : Finset β) : (a • s).dens = s.dens := by simp [dens] +@[to_additive (attr := simp)] lemma dens_inv (s : Finset α) : s⁻¹.dens = s.dens := by simp [dens] end Finset diff --git a/LeanAPAP/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean b/LeanAPAP/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean deleted file mode 100644 index e9933fb6e0..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean +++ /dev/null @@ -1,7 +0,0 @@ -import Mathlib.Algebra.Order.BigOperators.Group.Finset - -namespace Finset - -attribute [gcongr] sum_le_sum_of_subset_of_nonneg - -end Finset diff --git a/LeanAPAP/Mathlib/Algebra/Order/Field/Defs.lean b/LeanAPAP/Mathlib/Algebra/Order/Field/Defs.lean deleted file mode 100644 index b8bbd03c61..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Order/Field/Defs.lean +++ /dev/null @@ -1,6 +0,0 @@ -import Mathlib.Algebra.Order.Field.Defs - -variable {α : Type*} [LinearOrderedSemifield α] {a : α} - -lemma mul_inv_le_one : a * a⁻¹ ≤ 1 := by obtain rfl | ha := eq_or_ne a 0 <;> simp [*] -lemma inv_mul_le_one : a⁻¹ * a ≤ 1 := by obtain rfl | ha := eq_or_ne a 0 <;> simp [*] diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean index b780831c0e..9ea8a11b05 100644 --- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean +++ b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean @@ -1,4 +1,3 @@ -import LeanAPAP.Mathlib.Algebra.Order.Field.Defs import Mathlib.Analysis.SpecialFunctions.Pow.Real namespace Real diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index 3c3457c47c..26d73ae868 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/LeanAPAP/Physics/DRC.lean @@ -207,7 +207,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 rw [sum_mu _ hA₁, sum_mu _ hA₂, one_mul] rw [div_le_iff₀ (dLpNorm_conv_pos hp₀.ne' hB hA), ← le_div_iff₀' (zero_lt_two' ℝ)] simp only [apply_ite NNReal.toReal, indicate_apply, NNReal.coe_one, NNReal.coe_zero, mul_boole, - sum_ite_mem, univ_inter, mul_div_right_comm] + Fintype.sum_ite_mem, mul_div_right_comm] calc ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p ≤ ∑ x in (s p ε B₁ B₂ A)ᶜ, diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index cae9fa5bbc..cf697e5b8b 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -149,7 +149,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 _ ≤ sqrt (∑ i in T, ν i) * sqrt (∑ i in T, ν i * |(f ^ (2 * p)) i|) := (sum_sqrt_mul_sqrt_le _ (fun i ↦ ?_) fun i ↦ ?_) _ ≤ sqrt (∑ i in T, ν i) * sqrt (∑ i, ν i * |(f ^ (2 * p)) i|) := by - gcongr; exact sum_le_univ_sum_of_nonneg fun i ↦ by positivity + gcongr; exact T.subset_univ _ = sqrt (∑ i in T, ν i) * ‖f‖_[2 * ↑p, ν] ^ p := ?_ _ ≤ _ := by gcongr; exact mod_cast hf₁ any_goals positivity diff --git a/LeanAPAP/Prereqs/FourierTransform/Compact.lean b/LeanAPAP/Prereqs/FourierTransform/Compact.lean index cc08db5ed6..91dea1722b 100644 --- a/LeanAPAP/Prereqs/FourierTransform/Compact.lean +++ b/LeanAPAP/Prereqs/FourierTransform/Compact.lean @@ -49,7 +49,7 @@ lemma cft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : cft f ψ = ⟪ψ, f⟫ simp_rw [dL2Inner_eq_sum, cL2Inner_eq_expect, map_expect, map_mul, starRingEnd_self_apply, expect_mul, mul_expect, ← expect_sum_comm, mul_mul_mul_comm _ (conj $ f _), ← sum_mul, ← AddChar.inv_apply_eq_conj, ← map_neg_eq_inv, ← map_add_eq_mul, AddChar.sum_apply_eq_ite] - simp [add_neg_eq_zero, card_univ, Fintype.card_ne_zero, NNRat.smul_def (α := ℂ)] + simp [add_neg_eq_zero, card_univ, Fintype.card_ne_zero, NNRat.smul_def] /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/ @[simp] lemma dL2Norm_cft [MeasurableSpace α] [DiscreteMeasurableSpace α] (f : α → ℂ) : @@ -62,7 +62,7 @@ lemma cft_inversion (f : α → ℂ) (a : α) : ∑ ψ, cft f ψ * ψ a = f a := classical simp_rw [cft, cL2Inner_eq_expect, expect_mul, ← expect_sum_comm, mul_right_comm _ (f _), ← sum_mul, ← AddChar.inv_apply_eq_conj, inv_mul_eq_div, ← map_sub_eq_div, AddChar.sum_apply_eq_ite, sub_eq_zero, ite_mul, zero_mul, Fintype.expect_ite_eq] - simp [add_neg_eq_zero, card_univ, NNRat.smul_def (α := ℂ), Fintype.card_ne_zero] + simp [add_neg_eq_zero, card_univ, NNRat.smul_def (K := ℂ), Fintype.card_ne_zero] /-- **Fourier inversion** for the discrete Fourier transform. -/ lemma cft_inversion' (f : α → ℂ) : ∑ ψ, cft f ψ • ⇑ψ = f := by ext; simpa using cft_inversion _ _ @@ -115,8 +115,7 @@ lemma cft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime @[simp] lemma cft_trivNChar [DecidableEq α] : cft (trivNChar : α → ℂ) = 1 := by ext - simp [trivChar_apply, cft_apply, cL2Inner_eq_expect, ← map_expect, card_univ, - NNRat.smul_def (α := ℂ)] + simp [trivChar_apply, cft_apply, cL2Inner_eq_expect, ← map_expect, card_univ, NNRat.smul_def] @[simp] lemma cft_one : cft (1 : α → ℂ) = trivChar := dft_injective $ by classical rw [dft_trivChar, dft_cft, Pi.one_comp] @@ -125,7 +124,7 @@ variable [DecidableEq α] @[simp] lemma cft_indicate_zero (s : Finset α) : cft (𝟭 s) 0 = s.dens := by simp only [cft_apply, cL2Inner_eq_expect, expect_indicate, AddChar.zero_apply, map_one, one_mul, - dens, NNRat.smul_def (α := ℂ), div_eq_inv_mul] + dens, NNRat.smul_def (K := ℂ), div_eq_inv_mul] simp lemma cft_cconv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) : cft (f ∗ₙ g) ψ = cft f ψ * cft g ψ := by diff --git a/lake-manifest.json b/lake-manifest.json index d556b65b24..a9cc34c679 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "555be78e7f1df5d448c64e4282ece0dcc21214ff", + "rev": "09c50fb84c0b5e89b270ff20af6ae7e4bd61511e", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,