From 4ce31d2694410f2223ba9d2d340e5853a2e0936c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 20 Jul 2024 13:12:56 +0000 Subject: [PATCH] Bump mathlib --- LeanAPAP.lean | 1 - LeanAPAP/FiniteField/Basic.lean | 6 +- LeanAPAP/Mathlib/Algebra/BigOperators/Pi.lean | 7 +- LeanAPAP/Mathlib/Algebra/Group/AddChar.lean | 2 +- LeanAPAP/Physics/AlmostPeriodicity.lean | 181 +++++++++++------- LeanAPAP/Physics/DRC.lean | 2 +- LeanAPAP/Physics/Unbalancing.lean | 4 +- LeanAPAP/Prereqs/AddChar/Basic.lean | 2 +- LeanAPAP/Prereqs/AddChar/Defs.lean | 4 +- .../Prereqs/AddChar/PontryaginDuality.lean | 6 +- LeanAPAP/Prereqs/Chang.lean | 10 +- LeanAPAP/Prereqs/Convolution/Compact.lean | 4 +- .../Prereqs/Convolution/Discrete/Defs.lean | 7 +- LeanAPAP/Prereqs/Convolution/Order.lean | 4 +- LeanAPAP/Prereqs/Convolution/ThreeAP.lean | 2 +- LeanAPAP/Prereqs/Curlog.lean | 6 +- LeanAPAP/Prereqs/Energy.lean | 2 +- .../Prereqs/FourierTransform/Compact.lean | 4 +- .../Prereqs/FourierTransform/Discrete.lean | 7 +- LeanAPAP/Prereqs/Function/Indicator/Defs.lean | 2 +- LeanAPAP/Prereqs/LpNorm/Compact.lean | 2 +- LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean | 2 +- LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean | 4 +- LeanAPAP/Prereqs/LpNorm/Weighted.lean | 4 +- LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean | 44 ++--- LeanAPAP/Prereqs/Multinomial.lean | 18 +- LeanAPAP/Prereqs/WideDiag.lean | 62 ------ lake-manifest.json | 20 +- 28 files changed, 200 insertions(+), 219 deletions(-) delete mode 100644 LeanAPAP/Prereqs/WideDiag.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 4209c0953c..773591aab1 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -44,4 +44,3 @@ import LeanAPAP.Prereqs.LpNorm.Weighted import LeanAPAP.Prereqs.MarcinkiewiczZygmund import LeanAPAP.Prereqs.Multinomial import LeanAPAP.Prereqs.Rudin -import LeanAPAP.Prereqs.WideDiag diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean index 133428dc17..5908aa00e8 100644 --- a/LeanAPAP/FiniteField/Basic.lean +++ b/LeanAPAP/FiniteField/Basic.lean @@ -43,7 +43,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ : abs_mul, abs_of_nonneg, mul_div_cancel_left₀] <;> positivity · rw [lpNorm_mu hp''.symm.one_le hC, hp''.symm.coe.inv_sub_one, NNReal.coe_natCast, ← mul_rpow] rw [le_div_iff, mul_comm] at hγC - refine' rpow_le_rpow_of_nonpos _ hγC (neg_nonpos.2 _) + refine rpow_le_rpow_of_nonpos ?_ hγC (neg_nonpos.2 ?_) all_goals positivity · simp_rw [Nat.cast_mul, Nat.cast_two, p] rw [wlpNorm_const_right, mul_assoc, mul_left_comm, NNReal.coe_inv, inv_rpow, rpow_neg] @@ -55,7 +55,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ : push_cast norm_num rw [← neg_mul, rpow_mul, one_div, rpow_inv_le_iff_of_pos] - refine' (rpow_le_rpow_of_exponent_ge hγ hγ₁ $ neg_le_neg $ + exact (rpow_le_rpow_of_exponent_ge hγ hγ₁ $ neg_le_neg $ inv_le_inv_of_le (curlog_pos hγ hγ₁) $ Nat.le_ceil _).trans $ (rpow_neg_inv_curlog_le hγ.le hγ₁).trans $ exp_one_lt_d9.le.trans $ by norm_num all_goals positivity @@ -79,7 +79,7 @@ lemma di_in_ff (hε₀ : 0 < ε) (hε₁ : ε < 1) (hαA : α ≤ A.card / card (1 + ε / 32) * α ≤ ‖𝟭_[ℝ] A * μ V'‖_[⊤] := by obtain rfl | hA := A.eq_empty_or_nonempty · stop - refine' ⟨⊤, univ, _⟩ + refine ⟨⊤, univ, _⟩ rw [AffineSubspace.direction_top] simp only [AffineSubspace.top_coe, coe_univ, eq_self_iff_true, finrank_top, tsub_self, Nat.cast_zero, indicate_empty, zero_mul, lpNorm_zero, true_and_iff, diff --git a/LeanAPAP/Mathlib/Algebra/BigOperators/Pi.lean b/LeanAPAP/Mathlib/Algebra/BigOperators/Pi.lean index 1aac4d87da..542b7642a0 100644 --- a/LeanAPAP/Mathlib/Algebra/BigOperators/Pi.lean +++ b/LeanAPAP/Mathlib/Algebra/BigOperators/Pi.lean @@ -16,8 +16,7 @@ lemma filter_piFinset_card_of_mem [∀ a, DecidableEq (δ a)] (t : ∀ a, Finset have : (t' a).card = 1 := by simp [t'] have h₁ : ∏ b in univ.erase a, (t b).card = ∏ b, (t' b).card := by rw [← prod_erase (f := fun b ↦ (t' b).card) univ this] - refine' Finset.prod_congr rfl _ - intro b hb + refine Finset.prod_congr rfl fun b hb ↦ ?_ simp only [mem_erase, Ne, mem_univ, and_true_iff] at hb simp only [dif_neg (Ne.symm hb), t'] have h₂ : ∏ b, (t' b).card = ∏ b, ∑ i in t' b, 1 := by simp @@ -26,14 +25,14 @@ lemma filter_piFinset_card_of_mem [∀ a, DecidableEq (δ a)] (t : ∀ a, Finset congr 1 ext f simp only [mem_filter, mem_piFinset, t'] - refine' ⟨_, fun h ↦ _⟩ + refine ⟨?_, fun h ↦ ?_⟩ · rintro ⟨hf, rfl⟩ b split_ifs with h₁ · cases h₁ simp · exact hf _ have : f a = x := by simpa using h a - refine' ⟨fun b ↦ _, this⟩ + refine ⟨fun b ↦ ?_, this⟩ obtain rfl | hab := eq_or_ne a b · rwa [this] · simpa [dif_neg hab] using h b diff --git a/LeanAPAP/Mathlib/Algebra/Group/AddChar.lean b/LeanAPAP/Mathlib/Algebra/Group/AddChar.lean index 89c92d2aae..1fc9ae74ce 100644 --- a/LeanAPAP/Mathlib/Algebra/Group/AddChar.lean +++ b/LeanAPAP/Mathlib/Algebra/Group/AddChar.lean @@ -71,7 +71,7 @@ lemma sum_eq_ite (ψ : AddChar G R) : ∑ a, ψ a = if ψ = 0 then ↑(card G) e split_ifs with h · simp [h, card_univ] obtain ⟨x, hx⟩ := ne_one_iff.1 h - refine' eq_zero_of_mul_eq_self_left hx _ + refine eq_zero_of_mul_eq_self_left hx ?_ rw [Finset.mul_sum] exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index b332ad371e..4e6cedf1cb 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -4,12 +4,52 @@ import Mathlib.Data.Complex.ExponentialBounds import LeanAPAP.Prereqs.Convolution.Norm import LeanAPAP.Prereqs.MarcinkiewiczZygmund import LeanAPAP.Prereqs.Curlog -import LeanAPAP.Prereqs.WideDiag /-! # Almost-periodicity -/ +open scoped Pointwise + +namespace Finset +variable {α : Type*} [DecidableEq α] {s : Finset α} {k : ℕ} + +section Add +variable [Add α] + +lemma big_shifts_step1 (L : Finset (Fin k → α)) (hk : k ≠ 0) : + ∑ x in L + s.piDiag (Fin k), ∑ l in L, ∑ s in s.piDiag (Fin k), (if l + s = x then 1 else 0) + = L.card * s.card := by + simp only [@sum_comm _ _ _ _ (L + _), sum_ite_eq] + rw [sum_const_nat] + intro l hl + have := Fin.pos_iff_nonempty.1 (pos_iff_ne_zero.2 hk) + rw [sum_const_nat, mul_one, Finset.card_piDiag] + exact fun s hs ↦ if_pos (Finset.add_mem_add hl hs) + +end Add + +variable [AddCommGroup α] [Fintype α] + +lemma reindex_count (L : Finset (Fin k → α)) (hk : k ≠ 0) (hL' : L.Nonempty) (l₁ : Fin k → α) : + ∑ l₂ in L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 = + (univ.filter fun t ↦ (l₁ - fun _ ↦ t) ∈ L).card := + calc + _ = ∑ l₂ in L, ∑ t : α, ite ((l₁ - fun _ ↦ t) = l₂) 1 0 := by + refine sum_congr rfl fun l₂ hl₂ ↦ ?_ + rw [Fintype.sum_ite_eq_ite_exists] + simp only [mem_piDiag, mem_univ, eq_sub_iff_add_eq, true_and, sub_eq_iff_eq_add', + @eq_comm _ l₁] + rfl + rintro i j h rfl + cases k + · simp at hk + · simpa using congr_fun h 0 + _ = (univ.filter fun t ↦ (l₁ - fun _ ↦ t) ∈ L).card := by + simp only [sum_comm, sum_ite_eq, card_eq_sum_ones, sum_filter] + +end Finset + section variable {α : Type*} {g : α → ℝ} {c ε : ℝ} {A : Finset α} @@ -66,7 +106,7 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m) have := my_other_markov (by positivity) (by norm_num) (fun _ _ ↦ by positivity) h norm_num1 at this rw [Fintype.card_piFinsetConst, mul_comm, mul_one_div, Nat.cast_pow] at this - refine' this.trans_eq _ + refine this.trans_eq ?_ rw [l] congr with a : 3 refine pow_le_pow_iff_left ?_ ?_ ?_ <;> positivity @@ -76,7 +116,7 @@ lemma lemma28_part_one (hm : 1 ≤ m) (x : G) : (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := by let f' : G → ℂ := fun a ↦ f (x - a) - (mu A ∗ f) x - refine' (complex_marcinkiewicz_zygmund f' (by linarith only [hm]) _).trans_eq' _ + refine (complex_marcinkiewicz_zygmund f' (by linarith only [hm]) ?_).trans_eq' ?_ · intro i rw [Fintype.sum_piFinset_apply, sum_sub_distrib] simp only [sub_eq_zero, sum_const, indicate_apply] @@ -97,7 +137,7 @@ lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) : have hm' : 1 < 2 * m := (Nat.mul_le_mul_left 2 hm).trans_lt' $ by norm_num1 have hm'' : (1 : ℝ≥0∞) ≤ 2 * m := by rw [←hmeq, Nat.one_le_cast]; exact hm'.le gcongr - refine' (lpNorm_sub_le hm'' _ _).trans _ + refine (lpNorm_sub_le hm'' _ _).trans ?_ rw [lpNorm_translate, two_mul ‖f‖_[2 * m], add_le_add_iff_left] have hmeq' : ((2 * m : ℝ≥0) : ℝ≥0∞) = 2 * m := by rw [ENNReal.coe_mul, ENNReal.coe_two, ENNReal.coe_natCast] @@ -105,7 +145,7 @@ lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) : rw [←Nat.cast_two, ←Nat.cast_mul, Nat.one_lt_cast] exact hm' rw [←hmeq', conv_comm] - refine' (lpNorm_conv_le this.le _ _).trans _ + refine (lpNorm_conv_le this.le _ _).trans ?_ rw [l1Norm_mu hA, mul_one] lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) : @@ -113,7 +153,7 @@ lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 1 / 2 * ((k * ε) ^ (2 * m) * ∑ i : G, ‖f i‖ ^ (2 * m)) * ↑A.card ^ k := by have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two] have hm' : 2 * m ≠ 0 := by - refine' mul_ne_zero two_pos.ne' _ + refine mul_ne_zero two_pos.ne' ?_ rw [←pos_iff_ne_zero, ←Nat.succ_le_iff] exact hm rw [mul_pow (2 : ℝ), ←hmeq, ←lpNorm_pow_eq_sum hm' f, ←mul_assoc, ←mul_assoc, @@ -126,14 +166,11 @@ lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 have := pow_le_pow_of_le_one (show (0 : ℝ) ≤ 1 / 2 by norm_num) (show (1 / 2 : ℝ) ≤ 1 by norm_num) hm rwa [pow_one] at this - refine' (mul_le_mul_of_nonneg_right this _).trans' _ - · refine' pow_nonneg _ _ - refine' sq_nonneg _ + refine (mul_le_mul_of_nonneg_right this (by positivity)).trans' ?_ rw [←mul_pow] - refine' pow_le_pow_left _ _ _ - · positivity + refine pow_le_pow_left (by positivity) ?_ _ rw [mul_right_comm, mul_comm _ ε, mul_pow, ←mul_assoc, sq (k : ℝ), ←mul_assoc] - refine' mul_le_mul_of_nonneg_right _ (Nat.cast_nonneg k) + refine mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg k) rw [mul_right_comm, div_mul_eq_mul_div, one_mul, div_mul_eq_mul_div, le_div_iff' (zero_lt_two' ℝ), ←div_le_iff', ←mul_assoc] · norm_num1; exact hk @@ -143,13 +180,13 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) (A.card ^ k : ℝ) / 2 ≤ (l k m ε f A).card := by have : 0 < k := by rw [←@Nat.cast_pos ℝ] - refine' hk.trans_lt' _ - refine' div_pos (mul_pos (by norm_num1) _) (pow_pos hε _) + refine hk.trans_lt' ?_ + refine div_pos (mul_pos (by norm_num1) ?_) (pow_pos hε _) rw [Nat.cast_pos, ←Nat.succ_le_iff] exact hm rcases A.eq_empty_or_nonempty with (rfl | hA) · simp [zero_pow this.ne'] - refine' lemma28_markov hε hm _ + refine lemma28_markov hε hm ?_ have hm' : 2 * m ≠ 0 := by linarith have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two] rw [←hmeq, mul_pow] @@ -160,7 +197,7 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := lemma28_part_one hm - refine' (sum_le_sum fun x _ ↦ this x).trans _ + refine (sum_le_sum fun x _ ↦ this x).trans ?_ rw [←mul_sum] simp only [@sum_comm _ _ G] have (a : Fin k → G) (i : Fin k) : @@ -174,9 +211,9 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) (8 * m : ℝ) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := lemma28_part_two hm hA - refine' this.trans _ + refine this.trans ?_ simp only [sum_const, Fintype.card_piFinsetConst, nsmul_eq_mul, Nat.cast_pow] - refine' (lemma28_end hε hm hk).trans_eq' _ + refine (lemma28_end hε hm hk).trans_eq' ?_ simp only [mul_assoc, card_fin] lemma just_the_triangle_inequality {t : G} {a : Fin k → G} (ha : a ∈ l k m ε f A) @@ -189,13 +226,13 @@ lemma just_the_triangle_inequality {t : G} {a : Fin k → G} (ha : a ∈ l k m rw [l, Finset.mem_filter] at ha ; exact ha.2 have h₂ : ‖f₂ - k • (mu A ∗ f)‖_[2 * m] ≤ k * ε * ‖f‖_[2 * m] := by rw [l, Finset.mem_filter, LProp] at ha' - refine' ha'.2.trans_eq' _ + refine ha'.2.trans_eq' ?_ congr with i : 1 simp [sub_sub, f₂] have h₃ : f₂ = τ t f₁ := by ext i : 1 rw [translate_apply] - refine' Finset.sum_congr rfl fun j _ ↦ _ + refine Finset.sum_congr rfl fun j _ ↦ ?_ rw [sub_right_comm] have h₄₁ : ‖τ t f₁ - k • (mu A ∗ f)‖_[2 * m] = ‖τ (-t) (τ t f₁ - k • (mu A ∗ f))‖_[2 * m] := by rw [lpNorm_translate] @@ -205,53 +242,54 @@ lemma just_the_triangle_inequality {t : G} {a : Fin k → G} (ha : a ∈ l k m have h₅₁ : ‖τ (-t) (k • (mu A ∗ f)) - f₁‖_[2 * m] ≤ k * ε * ‖f‖_[2 * m] := by rwa [lpNorm_sub_comm, ←h₄, ←h₃] have : (0 : ℝ) < k := by positivity - refine' le_of_mul_le_mul_left _ this + refine le_of_mul_le_mul_left ?_ this rw [←nsmul_eq_mul, ← lpNorm_nsmul hp _ (_ - mu A ∗ f), nsmul_sub, ← translate_smul_right (-t) (mu A ∗ f) k, mul_assoc, mul_left_comm, two_mul ((k : ℝ) * _), ← mul_assoc] exact (lpNorm_sub_le_lpNorm_sub_add_lpNorm_sub hp _ _).trans (add_le_add h₅₁ h₁) lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) : - (∑ x in L + S.wideDiag k, ∑ l in L, ∑ s in S.wideDiag k, ite (l + s = x) (1 : ℝ) 0) ^ 2 ≤ - (L + S.wideDiag k).card * S.card * - ∑ l₁ in L, ∑ l₂ in L, ite (l₁ - l₂ ∈ fintypeWideDiag G k) 1 0 := by - refine' sq_sum_le_card_mul_sum_sq.trans _ - simp_rw [sq, sum_mul, @sum_comm _ _ _ _ (L + S.wideDiag k), boole_mul, sum_ite_eq, mul_assoc] - refine' mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _) + (∑ x in L + S.piDiag (Fin k), ∑ l in L, ∑ s in S.piDiag (Fin k), ite (l + s = x) (1 : ℝ) 0) ^ 2 + ≤ (L + S.piDiag (Fin k)).card * S.card * + ∑ l₁ in L, ∑ l₂ in L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 := by + refine sq_sum_le_card_mul_sum_sq.trans ?_ + simp_rw [sq, sum_mul, @sum_comm _ _ _ _ (L + S.piDiag (Fin k)), boole_mul, sum_ite_eq, mul_assoc] + refine mul_le_mul_of_nonneg_left ?_ (Nat.cast_nonneg _) have : ∀ f : (Fin k → G) → (Fin k → G) → ℝ, - ∑ x in L, ∑ y in S.wideDiag k, (if x + y ∈ L + S.wideDiag k then f x y else 0) = - ∑ x in L, ∑ y in S.wideDiag k, f x y := by - refine' fun f ↦ sum_congr rfl fun x hx ↦ _ + ∑ x in L, ∑ y in S.piDiag (Fin k), (if x + y ∈ L + S.piDiag (Fin k) then f x y else 0) = + ∑ x in L, ∑ y in S.piDiag (Fin k), f x y := by + refine fun f ↦ sum_congr rfl fun x hx ↦ ?_ exact sum_congr rfl fun y hy ↦ if_pos $ add_mem_add hx hy rw [this] have (x y) : - ∑ s₁ in S.wideDiag k, ∑ s₂ in S.wideDiag k, ite (y + s₂ = x + s₁) (1 : ℝ) 0 = - ite (x - y ∈ fintypeWideDiag G k) 1 0 * - ∑ s₁ in S.wideDiag k, ∑ s₂ in S.wideDiag k, ite (s₂ = x + s₁ - y) 1 0 := by + ∑ s₁ in S.piDiag (Fin k), ∑ s₂ in S.piDiag (Fin k), ite (y + s₂ = x + s₁) (1 : ℝ) 0 = + ite (x - y ∈ univ.piDiag (Fin k)) 1 0 * + ∑ s₁ in S.piDiag (Fin k), ∑ s₂ in S.piDiag (Fin k), ite (s₂ = x + s₁ - y) 1 0 := by simp_rw [mul_sum, boole_mul, ←ite_and] - refine' sum_congr rfl fun s₁ hs₁ ↦ _ - refine' sum_congr rfl fun s₂ hs₂ ↦ _ - refine' if_congr _ rfl rfl + refine sum_congr rfl fun s₁ hs₁ ↦ ?_ + refine sum_congr rfl fun s₂ hs₂ ↦ ?_ + refine if_congr ?_ rfl rfl rw [eq_sub_iff_add_eq', and_iff_right_of_imp] intro h - simp only [mem_wideDiag] at hs₁ hs₂ + simp only [mem_piDiag] at hs₁ hs₂ have : x - y = s₂ - s₁ := by rw [sub_eq_sub_iff_add_eq_add, ←h, add_comm] rw [this] obtain ⟨i, -, rfl⟩ := hs₁ obtain ⟨j, -, rfl⟩ := hs₂ exact mem_image.2 ⟨j - i, mem_univ _, rfl⟩ - simp_rw [@sum_comm _ _ _ _ (S.wideDiag k) L, this, sum_ite_eq'] + simp_rw [@sum_comm _ _ _ _ (S.piDiag (Fin k)) L, this, sum_ite_eq'] have : ∑ x in L, ∑ y in L, - ite (x - y ∈ fintypeWideDiag G k) (1 : ℝ) 0 * - ∑ z in S.wideDiag k, ite (x + z - y ∈ S.wideDiag k) 1 0 ≤ - ∑ x in L, ∑ y in L, ite (x - y ∈ fintypeWideDiag G k) 1 0 * (S.card : ℝ) := by - refine' sum_le_sum fun l₁ _ ↦ sum_le_sum fun l₂ _ ↦ _ - refine' mul_le_mul_of_nonneg_left _ (by split_ifs <;> norm_num) - refine' (sum_le_card_nsmul _ _ 1 _).trans_eq _ + ite (x - y ∈ univ.piDiag (Fin k)) (1 : ℝ) 0 * + ∑ z in S.piDiag (Fin k), ite (x + z - y ∈ S.piDiag (Fin k)) 1 0 ≤ + ∑ x in L, ∑ y in L, ite (x - y ∈ univ.piDiag (Fin k)) 1 0 * (S.card : ℝ) := by + refine sum_le_sum fun l₁ _ ↦ sum_le_sum fun l₂ _ ↦ ?_ + refine mul_le_mul_of_nonneg_left ?_ (by split_ifs <;> norm_num) + refine (sum_le_card_nsmul _ _ 1 ?_).trans_eq ?_ · intro x _; split_ifs <;> norm_num - rw [card_wideDiag hk] + have := Fin.pos_iff_nonempty.1 (pos_iff_ne_zero.2 hk) + rw [card_piDiag] simp only [nsmul_one] - refine' this.trans _ + refine this.trans ?_ simp_rw [←sum_mul, mul_comm] rfl @@ -264,22 +302,23 @@ lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0) rcases S.eq_empty_or_nonempty with (rfl | hS) · simpa only [card_empty, mul_zero, zero_le', and_true_iff] using hL' have hS' : 0 < S.card := by rwa [card_pos] - have : (L + S.wideDiag k).card ≤ (A + S).card ^ k := by - refine' (card_le_card (add_subset_add_right hL)).trans _ + have : (L + S.piDiag (Fin k)).card ≤ (A + S).card ^ k := by + refine (card_le_card (add_subset_add_right hL)).trans ?_ rw [←Fintype.card_piFinsetConst] - refine' card_le_card fun i hi ↦ _ - simp only [mem_add, mem_wideDiag, Fintype.mem_piFinset, exists_prop, exists_and_left, + refine card_le_card fun i hi ↦ ?_ + simp only [mem_add, mem_piDiag, Fintype.mem_piFinset, exists_prop, exists_and_left, exists_exists_and_eq_and] at hi ⊢ obtain ⟨y, hy, a, ha, rfl⟩ := hi intro j exact ⟨y j, hy _, a, ha, rfl⟩ rsuffices ⟨a, ha, h⟩ : ∃ a ∈ L, - L.card * S.card ≤ (L + S.wideDiag k).card * (univ.filter fun t : G ↦ (a - fun _ ↦ t) ∈ L).card + L.card * S.card ≤ (L + S.piDiag (Fin k)).card * (univ.filter fun t ↦ (a - fun _ ↦ t) ∈ L).card · exact ⟨a, ha, h.trans (Nat.mul_le_mul_right _ this)⟩ clear! A have : L.card ^ 2 * S.card ≤ - (L + S.wideDiag k).card * ∑ l₁ in L, ∑ l₂ in L, ite (l₁ - l₂ ∈ fintypeWideDiag G k) 1 0 := by - refine' Nat.le_of_mul_le_mul_left _ hS' + (L + S.piDiag (Fin k)).card * + ∑ l₁ in L, ∑ l₂ in L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 := by + refine Nat.le_of_mul_le_mul_left ?_ hS' rw [mul_comm, mul_assoc, ←sq, ←mul_pow, mul_left_comm, ←mul_assoc, ←big_shifts_step1 L hk] exact_mod_cast @big_shifts_step2 G _ _ _ _ _ L hk simp only [reindex_count L hk hL'] at this @@ -297,32 +336,32 @@ lemma T_bound (hK' : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ) * norm_num have hK : 0 < K := by positivity have : (0 : ℝ) < Ac ^ k := by positivity - refine' le_of_mul_le_mul_left _ this + refine le_of_mul_le_mul_left ?_ this have : (Ac : ℝ) ^ k ≤ K * Lc := by rw [div_le_iff'] at h₂ - refine' h₂.trans (mul_le_mul_of_nonneg_right hK' (Nat.cast_nonneg _)) + refine h₂.trans (mul_le_mul_of_nonneg_right hK' (Nat.cast_nonneg _)) exact zero_lt_two rw [neg_mul, neg_div, Real.rpow_neg hK.le, mul_left_comm, inv_mul_le_iff (Real.rpow_pos_of_pos hK _)] - refine' (mul_le_mul_of_nonneg_right this (Nat.cast_nonneg _)).trans _ + refine (mul_le_mul_of_nonneg_right this (Nat.cast_nonneg _)).trans ?_ rw [mul_assoc] rw [←@Nat.cast_le ℝ, Nat.cast_mul] at h₁ - refine' (mul_le_mul_of_nonneg_left h₁ hK.le).trans _ + refine (mul_le_mul_of_nonneg_left h₁ hK.le).trans ?_ rw [Nat.cast_mul, ←mul_assoc, ←mul_assoc, Nat.cast_pow] - refine' mul_le_mul_of_nonneg_right _ (Nat.cast_nonneg _) - refine' (mul_le_mul_of_nonneg_left (pow_le_pow_left (Nat.cast_nonneg _) h₃ k) hK.le).trans _ + refine mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg _) + refine (mul_le_mul_of_nonneg_left (pow_le_pow_left (Nat.cast_nonneg _) h₃ k) hK.le).trans ?_ rw [mul_pow, ←mul_assoc, ←pow_succ'] - refine' mul_le_mul_of_nonneg_right _ (pow_nonneg (Nat.cast_nonneg _) _) + refine mul_le_mul_of_nonneg_right ?_ (pow_nonneg (Nat.cast_nonneg _) _) rw [←Real.rpow_natCast] - refine' Real.rpow_le_rpow_of_exponent_le (one_le_two.trans hK') _ + refine Real.rpow_le_rpow_of_exponent_le (one_le_two.trans hK') ?_ rw [Nat.cast_add_one, ←le_sub_iff_add_le, hk'] - refine' (Nat.ceil_lt_add_one _).le.trans _ + refine (Nat.ceil_lt_add_one ?_).le.trans ?_ · positivity have : (1 : ℝ) ≤ 128 * (m / ε ^ 2) := by rw [div_eq_mul_one_div] - refine' one_le_mul_of_one_le_of_one_le (by norm_num1) _ - refine' one_le_mul_of_one_le_of_one_le (Nat.one_le_cast.2 hm) _ - refine' one_le_one_div (by positivity) _ + refine one_le_mul_of_one_le_of_one_le (by norm_num1) ?_ + refine one_le_mul_of_one_le_of_one_le (Nat.one_le_cast.2 hm) ?_ + refine one_le_one_div (by positivity) ?_ rw [sq_le_one_iff hε.le] exact hε' rw [mul_div_assoc, mul_div_assoc] @@ -335,12 +374,12 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) ( K ^ (-512 * m / ε ^ 2 : ℝ) * S.card ≤ T.card ∧ ∀ t ∈ T, ‖τ t (mu A ∗ f) - mu A ∗ f‖_[2 * m] ≤ ε * ‖f‖_[2 * m] := by obtain rfl | hA := A.eq_empty_or_nonempty - · refine' ⟨univ, _, fun t _ ↦ _⟩ + · refine ⟨univ, ?_, fun t _ ↦ ?_⟩ · have : K ^ ((-512 : ℝ) * m / ε ^ 2) ≤ 1 := by - refine' Real.rpow_le_one_of_one_le_of_nonpos (one_le_two.trans hK') _ + refine Real.rpow_le_one_of_one_le_of_nonpos (one_le_two.trans hK') ?_ rw [neg_mul, neg_div, Right.neg_nonpos_iff] positivity - refine' (mul_le_mul_of_nonneg_right this (Nat.cast_nonneg _)).trans _ + refine (mul_le_mul_of_nonneg_right this (Nat.cast_nonneg _)).trans ?_ rw [one_mul, Nat.cast_le] exact card_le_univ _ simp only [mu_empty, zero_conv, translate_zero_right, sub_self, lpNorm_zero] @@ -351,11 +390,9 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) ( have : (A.card : ℝ) ^ k / 2 ≤ L.card := lemma28 (half_pos hε) hm (Nat.le_ceil _) have hL : L.Nonempty := by rw [←card_pos, ←@Nat.cast_pos ℝ] - refine' this.trans_lt' _ - refine' div_pos (pow_pos _ _) zero_lt_two - rwa [Nat.cast_pos, card_pos] + exact this.trans_lt' (by positivity) obtain ⟨a, ha, hL'⟩ := big_shifts S _ hk hL (filter_subset _ _) - refine' ⟨univ.filter fun t : G ↦ (a + fun _ ↦ -t) ∈ L, _, _⟩ + refine ⟨univ.filter fun t : G ↦ (a + fun _ ↦ -t) ∈ L, ?_, ?_⟩ · simp_rw [sub_eq_add_neg] at hL' exact T_bound hK' L.card S.card A.card (A + S).card _ rfl hL' this hK hA.card_pos hε hε' hm intro t ht diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index 42918e4991..4edcba1f1e 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/LeanAPAP/Physics/DRC.lean @@ -23,7 +23,7 @@ private lemma lemma_0 (p : ℕ) (B₁ B₂ A : Finset G) (f : G → ℝ) : @sum_comm _ _ (Fin p → G), sum_dconv_mul, dconv_apply_sub, Fintype.sum_pow, map_indicate] congr with b₁ congr with b₂ - refine' Fintype.sum_equiv (Equiv.neg $ Fin p → G) _ _ fun s ↦ _ + refine Fintype.sum_equiv (Equiv.neg $ Fin p → G) _ _ fun s ↦ ?_ rw [←smul_mul_assoc, ←smul_mul_smul, card_smul_mu_apply, card_smul_mu_apply, indicate_inter_apply, indicate_inter_apply, mul_mul_mul_comm, prod_mul_distrib] simp [c, indicate_inf_apply, ←translate_indicate, sub_eq_add_neg, mul_assoc, add_comm] diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index 068af0d674..fa24b959ec 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -30,7 +30,7 @@ lemma pow_inner_nonneg' {f : G → ℂ} (hf : f = g ○ g) (hν : (↑) ∘ ν = simp only [mem_filter, mem_univ, true_and_iff] rintro _ _ rfl rfl - refine' (sum_congr rfl fun _ _ ↦ sum_congr rfl $ this _).trans _ + refine (sum_congr rfl fun _ _ ↦ sum_congr rfl $ this _).trans ?_ simp_rw [dconv_apply_sub, sum_fiberwise, ←univ_product_univ, sum_product] simp only [sum_pow', sum_mul_sum, map_mul, starRingEnd_self_apply, Fintype.piFinset_univ, ←Complex.conj_mul', sum_product, map_sum, map_prod, @@ -84,7 +84,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 _ = _ := ?_ rw [wlpNorm_pow_eq_sum hp₁.pos.ne'] dsimp - refine' sum_congr rfl fun i _ ↦ _ + refine sum_congr rfl fun i _ ↦ ?_ rw [←abs_of_nonneg ((Nat.Odd.sub_odd hp₁ odd_one).pow_nonneg $ f _), abs_pow, pow_sub_one_mul hp₁.pos.ne'] simp [l2Inner_eq_sum, ←sum_add_distrib, ←mul_add, ←pow_sub_one_mul hp₁.pos.ne' (f _), diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean index edbc0e0453..300aaf5e24 100644 --- a/LeanAPAP/Prereqs/AddChar/Basic.lean +++ b/LeanAPAP/Prereqs/AddChar/Basic.lean @@ -28,7 +28,7 @@ lemma expect_eq_ite (ψ : AddChar G R) : 𝔼 a, ψ a = if ψ = 0 then 1 else 0 split_ifs with h · simp [h, card_univ, univ_nonempty] obtain ⟨x, hx⟩ := ne_one_iff.1 h - refine' eq_zero_of_mul_eq_self_left hx _ + refine eq_zero_of_mul_eq_self_left hx ?_ rw [Finset.mul_expect] exact Fintype.expect_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul _ _ _).symm diff --git a/LeanAPAP/Prereqs/AddChar/Defs.lean b/LeanAPAP/Prereqs/AddChar/Defs.lean index 014f1e31e7..60f831cc68 100644 --- a/LeanAPAP/Prereqs/AddChar/Defs.lean +++ b/LeanAPAP/Prereqs/AddChar/Defs.lean @@ -20,7 +20,7 @@ variable [Finite G] [NormedField R] (ψ.toMonoidHom.isOfFinOrder $ isOfFinOrder_of_finite _).norm_eq_one @[simp] lemma coe_ne_zero (ψ : AddChar G R) : (ψ : G → R) ≠ 0 := - Function.ne_iff.2 ⟨0, fun h ↦ by simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ⟩ + ne_iff.2 ⟨0, fun h ↦ by simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ⟩ end NormedField @@ -56,7 +56,7 @@ protected def directSum (ψ : ∀ i, AddChar (π i) R) : AddChar (⨁ i, π i) R lemma directSum_injective : Injective (AddChar.directSum : (∀ i, AddChar (π i) R) → AddChar (⨁ i, π i) R) := by - refine' AddChar.toAddMonoidHomEquiv.symm.injective.comp $ DirectSum.toAddMonoid_injective.comp _ + refine AddChar.toAddMonoidHomEquiv.symm.injective.comp $ DirectSum.toAddMonoid_injective.comp ?_ rintro ψ χ h simpa [Function.funext_iff] using h diff --git a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean index 98fc1599cb..9770d1904b 100644 --- a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean +++ b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean @@ -128,8 +128,8 @@ def circleEquivComplex [Finite α] : AddChar α circle ≃+ AddChar α ℂ where /-- `ZMod n` is (noncanonically) isomorphic to its group of characters. -/ def zmodAddEquiv (hn : n ≠ 0) : ZMod n ≃+ AddChar (ZMod n) ℂ := by haveI : NeZero n := ⟨hn⟩ - refine' AddEquiv.ofBijective - (circleEquivComplex.toAddMonoidHom.comp $ AddChar.toAddMonoidHom $ zmodHom n) _ + refine AddEquiv.ofBijective + (circleEquivComplex.toAddMonoidHom.comp $ AddChar.toAddMonoidHom $ zmodHom n) ?_ rw [Fintype.bijective_iff_injective_and_card, card_eq] exact ⟨circleEquivComplex.injective.comp $ zmod_injective hn, rfl⟩ @@ -154,7 +154,7 @@ variable {α} lemma complexBasis_apply (ψ : AddChar α ℂ) : complexBasis α ψ = ψ := by rw [coe_complexBasis] lemma exists_apply_ne_zero : (∃ ψ : AddChar α ℂ, ψ a ≠ 1) ↔ a ≠ 0 := by - refine' ⟨_, fun ha ↦ _⟩ + refine ⟨?_, fun ha ↦ ?_⟩ · rintro ⟨ψ, hψ⟩ rfl exact hψ ψ.map_zero_eq_one classical diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean index a69ede44b8..b5191cded3 100644 --- a/LeanAPAP/Prereqs/Chang.lean +++ b/LeanAPAP/Prereqs/Chang.lean @@ -21,7 +21,7 @@ lemma α_nonneg (f : G → ℂ) : 0 ≤ α f := by unfold α; positivity lemma α_pos (hf : f ≠ 0) : 0 < α f := by unfold α; positivity lemma α_le_one (f : G → ℂ) : α f ≤ 1 := by - refine' div_le_one_of_le (div_le_of_nonneg_of_le_mul _ _ _) _ + refine div_le_one_of_le (div_le_of_nonneg_of_le_mul ?_ ?_ ?_) ?_ any_goals positivity rw [l1Norm_eq_sum, l2Norm_sq_eq_sum] exact sq_sum_le_card_mul_sum_sq @@ -149,12 +149,12 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) : have : 0 < α f := α_pos hf set β := ⌈curlog (α f)⌉₊ have hβ : 0 < β := Nat.ceil_pos.2 (curlog_pos (α_pos hf) $ α_le_one _) - refine' le_of_pow_le_pow_left hβ.ne' zero_le' $ Nat.cast_le.1 $ le_of_mul_le_mul_right _ + refine le_of_pow_le_pow_left hβ.ne' zero_le' $ Nat.cast_le.1 $ le_of_mul_le_mul_right ?_ (by positivity : 0 < ↑Δ.card ^ β * (η ^ (2 * β) * α f)) push_cast rw [←mul_assoc, ←pow_add, ←two_mul] - refine' ((spec_hoelder hη.le hΔη hβ.ne').trans $ hΔ.boringEnergy_le _).trans _ - refine' le_trans _ $ mul_le_mul_of_nonneg_right (pow_le_pow_left _ (Nat.le_ceil _) _) _ + refine ((spec_hoelder hη.le hΔη hβ.ne').trans $ hΔ.boringEnergy_le _).trans ?_ + refine le_trans ?_ $ mul_le_mul_of_nonneg_right (pow_le_pow_left ?_ (Nat.le_ceil _) _) ?_ rw [mul_right_comm, div_pow, mul_pow, mul_pow, exp_one_pow, ←pow_mul, mul_div_assoc] calc _ = (changConst * Δ.card * β) ^ β := by ring @@ -162,7 +162,7 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) : _ ≤ (changConst * Δ.card * β) ^ β * ((η / η) ^ (2 * β) * α f * exp β) := by rw [div_self hη.ne', one_pow, one_mul] _ = _ := by ring - refine' le_mul_of_one_le_right (by positivity) _ + refine le_mul_of_one_le_right (by positivity) ?_ rw [←inv_pos_le_iff_one_le_mul'] exact inv_le_exp_curlog.trans $ exp_monotone $ Nat.le_ceil _ all_goals positivity diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean index f74fe8af82..79cf005c94 100644 --- a/LeanAPAP/Prereqs/Convolution/Compact.lean +++ b/LeanAPAP/Prereqs/Convolution/Compact.lean @@ -502,9 +502,9 @@ lemma support_iterNConv_subset (f : α → β) : ∀ n, support (f ∗^ₙ n) -- · simp [apply_ite card, eq_comm] -- simp_rw [iterNConv_succ, nconv_eq_expect_sub', ih, indicate_apply, boole_mul, expect_ite, filter_univ_mem, -- expect_const_zero, add_zero, ←Nat.cast_expect, ←Finset.card_sigma, Nat.cast_inj] --- refine' Finset.card_bij (fun f _ ↦ Fin.cons f.1 f.2) _ _ _ +-- refine Finset.card_bij (fun f _ ↦ Fin.cons f.1 f.2) _ _ _ -- · simp only [Fin.expect_cons, eq_sub_iff_add_eq', mem_sigma, mem_filter, mem_piFinset, and_imp] --- refine' fun bf hb hf ha ↦ ⟨Fin.cases _ _, ha⟩ +-- refine fun bf hb hf ha ↦ ⟨Fin.cases _ _, ha⟩ -- · exact hb -- · simpa only [Fin.cons_succ] -- · simp only [Sigma.ext_iff, Fin.cons_eq_cons, heq_iff_eq, imp_self, imp_true_iff, forall_const, diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean index 8aa7b59e92..26dd42aab3 100644 --- a/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean +++ b/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean @@ -164,9 +164,8 @@ lemma mul_smul_conv_comm [Monoid γ] [DistribMulAction γ β] [IsScalarTower γ lemma conv_assoc (f g h : α → β) : f ∗ g ∗ h = f ∗ (g ∗ h) := by ext a simp only [sum_mul, mul_sum, conv_apply, sum_sigma'] - refine' sum_nbij' (fun ⟨(_b, c), (d, e)⟩ ↦ ⟨(d, e + c), (e, c)⟩) - (fun ⟨(b, _c), (d, e)⟩ ↦ ⟨(b + d, e), (b, d)⟩) _ _ _ _ _ <;> - aesop (add simp [add_assoc, mul_assoc]) + apply sum_nbij' (fun ⟨(_b, c), (d, e)⟩ ↦ ⟨(d, e + c), (e, c)⟩) + (fun ⟨(b, _c), (d, e)⟩ ↦ ⟨(b + d, e), (b, d)⟩) <;> aesop (add simp [add_assoc, mul_assoc]) lemma conv_right_comm (f g h : α → β) : f ∗ g ∗ h = f ∗ h ∗ g := by rw [conv_assoc, conv_assoc, conv_comm g] @@ -200,7 +199,7 @@ lemma map_dconv (f g : α → ℝ≥0) (a : α) : (↑((f ○ g) a) : ℝ) = (( Function.comp_apply] lemma conv_eq_sum_sub (f g : α → β) (a : α) : (f ∗ g) a = ∑ t, f (a - t) * g t := by - rw [conv_apply]; refine' sum_nbij' Prod.snd (fun b ↦ (a - b, b)) _ _ _ _ _ <;> aesop + rw [conv_apply]; apply sum_nbij' Prod.snd (fun b ↦ (a - b, b)) <;> aesop lemma dconv_eq_sum_sub (f g : α → β) (a : α) : (f ○ g) a = ∑ t, f (a - t) * conj (g (-t)) := by simp [←conv_conjneg, conv_eq_sum_sub] diff --git a/LeanAPAP/Prereqs/Convolution/Order.lean b/LeanAPAP/Prereqs/Convolution/Order.lean index 14a1b0a8b0..1f440e50ff 100644 --- a/LeanAPAP/Prereqs/Convolution/Order.lean +++ b/LeanAPAP/Prereqs/Convolution/Order.lean @@ -22,7 +22,7 @@ variable [StrictOrderedCommSemiring β] [StarRing β] [StarOrderedRing β] {f g --TODO: Those can probably be generalised to `OrderedCommSemiring` but we don't really care @[simp] lemma support_conv (hf : 0 ≤ f) (hg : 0 ≤ g) : support (f ∗ g) = support f + support g := by - refine' (support_conv_subset _ _).antisymm _ + refine (support_conv_subset _ _).antisymm ?_ rintro _ ⟨a, ha, b, hb, rfl⟩ rw [mem_support, conv_apply_add] exact ne_of_gt $ sum_pos' (fun c _ ↦ mul_nonneg (hf _) $ hg _) ⟨0, mem_univ _, @@ -36,7 +36,7 @@ lemma conv_pos (hf : 0 < f) (hg : 0 < g) : 0 < f ∗ g := by rw [Pi.lt_def] at hf hg ⊢ obtain ⟨hf, a, ha⟩ := hf obtain ⟨hg, b, hb⟩ := hg - refine' ⟨conv_nonneg hf hg, a + b, _⟩ + refine ⟨conv_nonneg hf hg, a + b, ?_⟩ rw [conv_apply_add] exact sum_pos' (fun c _ ↦ mul_nonneg (hf _) $ hg _) ⟨0, by simpa using mul_pos ha hb⟩ diff --git a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean index 6774eb8498..1c34b0f47a 100644 --- a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean +++ b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean @@ -21,7 +21,7 @@ lemma ThreeAPFree.l2Inner_mu_conv_mu_mu_two_smul_mu (hG : Odd (card G)) Finset.sum_eq_zero, Finset.sum_eq_zero, add_zero, add_zero, pow_succ', mul_inv, mul_inv_cancel_left₀] · exact Nat.cast_ne_zero.2 hs'.card_pos.ne' - · refine' fun i hi ↦ not_ne_iff.1 fun h ↦ (mem_offDiag.1 hi).2.2 _ + · refine fun i hi ↦ not_ne_iff.1 fun h ↦ (mem_offDiag.1 hi).2.2 ?_ simp_rw [mul_ne_zero_iff, ←mem_support, support_mu, mem_coe, mem_image, two_smul] at h obtain ⟨b, hb, hab⟩ := h.2 obtain rfl := hs h.1.1 hb h.1.2 hab.symm diff --git a/LeanAPAP/Prereqs/Curlog.lean b/LeanAPAP/Prereqs/Curlog.lean index d5445260a4..bb32959efa 100644 --- a/LeanAPAP/Prereqs/Curlog.lean +++ b/LeanAPAP/Prereqs/Curlog.lean @@ -51,11 +51,11 @@ lemma rpow_neg_inv_curlog_le (hx : 0 ≤ x) (hx' : x ≤ 1) : x ^ (-(curlog x) · simp have : -1 / log (1 / x) ≤ -1 / curlog x := by rw [neg_div, neg_div, neg_le_neg_iff] - refine' one_div_le_one_div_of_le _ (log_one_div_le_curlog hx.le) - refine' log_pos _ + refine one_div_le_one_div_of_le ?_ (log_one_div_le_curlog hx.le) + refine log_pos ?_ rwa [lt_div_iff hx, one_mul] rw [←one_div, ←neg_div] - refine' (rpow_le_rpow_of_exponent_ge hx hx'.le this).trans _ + refine (rpow_le_rpow_of_exponent_ge hx hx'.le this).trans ?_ rw [one_div, log_inv, rpow_def_of_pos hx, neg_div_neg_eq, mul_one_div, div_self] exact log_ne_zero_of_pos_of_ne_one hx hx'.ne diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean index 30dbe135a3..cb3effc891 100644 --- a/LeanAPAP/Prereqs/Energy.lean +++ b/LeanAPAP/Prereqs/Energy.lean @@ -34,7 +34,7 @@ lemma boringEnergy_eq (n : ℕ) (s : Finset G) : boringEnergy n s = ∑ x, (𝟭 rw [←Finset.sum_fiberwise _ fun f : Fin n → G ↦ ∑ i, f i] congr with x rw [indicate_iterConv_apply, sq, ←nsmul_eq_mul, ←sum_const] - refine' sum_congr rfl fun f hf ↦ _ + refine sum_congr rfl fun f hf ↦ ?_ simp_rw [(mem_filter.1 hf).2, eq_comm] @[simp] lemma boringEnergy_zero (s : Finset G) : boringEnergy 0 s = 1 := by simp [boringEnergy] diff --git a/LeanAPAP/Prereqs/FourierTransform/Compact.lean b/LeanAPAP/Prereqs/FourierTransform/Compact.lean index 41d0835f75..ff56bf2389 100644 --- a/LeanAPAP/Prereqs/FourierTransform/Compact.lean +++ b/LeanAPAP/Prereqs/FourierTransform/Compact.lean @@ -174,7 +174,7 @@ lemma nlpNorm_nconv_le_nlpNorm_ndconv (hn₀ : n ≠ 0) (hn : Even n) (f : α map_mul, Fintype.sum_pow, Fintype.sum_mul_sum] sorry -- simp only [@expect_comm _ _ α, ←mul_expect, prod_mul_prod_comm] - -- refine' (norm_expect_le _ _).trans_eq (Complex.ofReal_injective _) + -- refine (norm_expect_le _ _).trans_eq (Complex.ofReal_injective _) -- simp only [norm_mul, norm_prod, RCLike.norm_conj, ←pow_mul] -- push_cast -- have : ∀ f g : Fin n → AddChar α ℂ, 0 ≤ ∑ a, ∏ i, conj (f i a) * g i a := by @@ -191,7 +191,7 @@ lemma nlpNorm_nconv_le_nlpNorm_ndconv (hn₀ : n ≠ 0) (hn : Even n) (f : α -- ext -- rw [←Complex.eq_coe_norm_of_nonneg (this _ _)] -- simp only [@expect_comm _ _ α, mul_expect, map_prod, map_mul, RCLike.conj_conj, ←prod_mul_distrib] - -- refine' expect_congr rfl fun x _ ↦ expect_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _ + -- refine expect_congr rfl fun x _ ↦ expect_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _ -- ring --TODO: Can we unify with `nlpNorm_nconv_le_nlpNorm_ndconv`? diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean index 7e7d4985da..7cd8070298 100644 --- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean +++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean @@ -88,7 +88,7 @@ lemma dft_conj (f : α → ℂ) (ψ : AddChar α ℂ) : dft (conj f) ψ = conj ( lemma dft_conjneg_apply (f : α → ℂ) (ψ : AddChar α ℂ) : dft (conjneg f) ψ = conj (dft f ψ) := by simp only [dft_apply, l2Inner_eq_sum, conjneg_apply, map_sum, map_mul, RCLike.conj_conj] - refine' Fintype.sum_equiv (Equiv.neg α) _ _ fun i ↦ _ + refine Fintype.sum_equiv (Equiv.neg α) _ _ fun i ↦ ?_ simp only [Equiv.neg_apply, ←inv_apply_eq_conj, ←inv_apply', inv_apply] @[simp] @@ -166,7 +166,7 @@ lemma lpNorm_conv_le_lpNorm_dconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → -- simp_rw [pow_mul', ←norm_pow _ n, Complex.ofReal_pow, ←Complex.conj_mul', map_pow, map_sum, -- map_mul, Fintype.sum_pow, Fintype.sum_mul_sum] -- simp only [@sum_comm _ _ α, ←mul_sum, prod_mul_prod_comm] --- refine' (norm_sum_le _ _).trans_eq (Complex.ofReal_injective _) +-- refine (norm_sum_le _ _).trans_eq (Complex.ofReal_injective _) -- simp only [norm_mul, norm_prod, RCLike.norm_conj, ←pow_mul] -- push_cast -- have : ∀ f g : Fin n → AddChar α ℂ, 0 ≤ ∑ a, ∏ i, conj (f i a) * g i a := by @@ -183,7 +183,7 @@ lemma lpNorm_conv_le_lpNorm_dconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → -- ext -- rw [←Complex.eq_coe_norm_of_nonneg (this _ _)] -- simp only [@sum_comm _ _ α, mul_sum, map_prod, map_mul, RCLike.conj_conj, ←prod_mul_distrib] --- refine' sum_congr rfl fun x _ ↦ sum_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _ +-- refine sum_congr rfl fun x _ ↦ sum_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _ -- ring --TODO: Can we unify with `lpNorm_conv_le_lpNorm_dconv`? @@ -191,4 +191,3 @@ lemma lpNorm_conv_le_lpNorm_dconv' (hn₀ : n ≠ 0) (hn : Even n) (f : α → ‖f ∗ f‖_[n] ≤ ‖f ○ f‖_[n] := by simpa only [←Complex.coe_comp_conv, ←Complex.coe_comp_dconv, Complex.lpNorm_coe_comp] using lpNorm_conv_le_lpNorm_dconv hn₀ hn ((↑) ∘ f) - diff --git a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean index 0c78e4ef64..a8fb64c268 100644 --- a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean +++ b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean @@ -177,7 +177,7 @@ variable [Nontrivial β] [CharZero β] {a : α} @[simp] lemma mu_apply_eq_zero : μ_[β] s a = 0 ↔ a ∉ s := by simp only [mu_apply, mul_boole, ite_eq_right_iff, inv_eq_zero, Nat.cast_eq_zero, card_eq_zero] - refine' imp_congr_right fun ha ↦ _ + refine imp_congr_right fun ha ↦ ?_ simp only [ne_empty_of_mem ha] lemma mu_apply_ne_zero : μ_[β] s a ≠ 0 ↔ a ∈ s := mu_apply_eq_zero.not_left diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean index 45a35e470c..dce1cdde2a 100644 --- a/LeanAPAP/Prereqs/LpNorm/Compact.lean +++ b/LeanAPAP/Prereqs/LpNorm/Compact.lean @@ -495,7 +495,7 @@ lemma nlpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖ all_goals positivity lemma nlpNorm_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖ₙ_[p] = s.dens ^ (p⁻¹ : ℝ) := by - refine' (eq_rpow_inv _ _ _).2 (nlpNorm_rpow_indicate _ _) <;> positivity + refine (eq_rpow_inv ?_ ?_ ?_).2 (nlpNorm_rpow_indicate ?_ _) <;> positivity lemma nlpNorm_pow_indicate {p : ℕ} (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖ₙ_[p] ^ (p : ℝ) = s.dens := by diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean index 03b76cf403..fdde91df3e 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean @@ -88,7 +88,7 @@ lemma lpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖_[p sum_boole, this, zero_rpow, filter_mem_eq_inter] lemma lpNorm_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖_[p] = s.card ^ (p⁻¹ : ℝ) := by - refine' (eq_rpow_inv _ _ _).2 (lpNorm_rpow_indicate _ _) <;> positivity + refine (eq_rpow_inv ?_ ?_ ?_).2 (lpNorm_rpow_indicate ?_ _) <;> positivity lemma lpNorm_pow_indicate {p : ℕ} (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖_[p] ^ (p : ℝ) = s.card := by diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean index f9a2f651de..84a4186628 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean @@ -536,8 +536,8 @@ lemma lpNorm_prod_le {s : Finset ι} (hs : s.Nonempty) {p : ι → ℝ≥0} (hp simp [←hpq] simp_rw [prod_cons] rw [sum_cons, ←inv_inv (∑ _ ∈ _, _ : ℝ≥0)] at hpq - refine' - (lpNorm_mul_le (hp _) (inv_ne_zero (sum_pos (fun _ _ ↦ _) hs).ne') _ hpq _ _).trans + refine + (lpNorm_mul_le (hp _) (inv_ne_zero (sum_pos (fun _ _ ↦ ?_) hs).ne') _ hpq _ _).trans (mul_le_mul_of_nonneg_left (ih hs _ (inv_inv _).symm) lpNorm_nonneg) exact pos_iff_ne_zero.2 (inv_ne_zero $ hp _) diff --git a/LeanAPAP/Prereqs/LpNorm/Weighted.lean b/LeanAPAP/Prereqs/LpNorm/Weighted.lean index 2c4791ecfb..1cf979878b 100644 --- a/LeanAPAP/Prereqs/LpNorm/Weighted.lean +++ b/LeanAPAP/Prereqs/LpNorm/Weighted.lean @@ -80,8 +80,8 @@ section one_le lemma wlpNorm_add_le (hp : 1 ≤ p) (w : ι → ℝ≥0) (f g : ∀ i, α i) : ‖f + g‖_[p, w] ≤ ‖f‖_[p, w] + ‖g‖_[p, w] := by unfold wlpNorm - refine' (lpNorm_add_le (by exact_mod_cast hp) _ _).trans' - (lpNorm_mono (fun i ↦ by dsimp; positivity) fun i ↦ _) + refine (lpNorm_add_le (by exact_mod_cast hp) _ _).trans' + (lpNorm_mono (fun i ↦ by dsimp; positivity) fun i ↦ ?_) dsimp rw [←smul_add] exact smul_le_smul_of_nonneg_left (norm_add_le _ _) (zero_le _) diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean index 3c14f19906..4f1666a031 100644 --- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean +++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean @@ -64,7 +64,7 @@ private lemma step_two_aux (A : Finset G) (f : G → ℝ) (ε : Fin n → ℝ) exact (h i).symm have h₂ : ∀ a ∈ (A^^n) ×ˢ (A^^n), swapper (swapper a) = a := fun a _ ↦ by ext <;> simp only <;> split_ifs <;> rfl - refine' sum_nbij' swapper swapper h₁ h₁ h₂ h₂ _ + refine sum_nbij' swapper swapper h₁ h₁ h₂ h₂ ?_ · rintro ⟨a, b⟩ _ congr with i : 1 simp only [Pi.mul_apply, Pi.sub_apply, Function.comp_apply] @@ -94,10 +94,10 @@ private lemma step_three (f : G → ℝ) : (multinomial univ k * ∏ t, (f (a t) - f (b t)) ^ k t) * ∑ ε in ({-1, 1} : Finset ℝ)^^n, ∏ t, ε t ^ k t := by simp only [@sum_comm _ _ (Fin n → ℝ) _ _ (A^^n), ←Complex.abs_pow, multinomial_expansion'] - refine' sum_congr rfl fun a _ ↦ _ - refine' sum_congr rfl fun b _ ↦ _ + refine sum_congr rfl fun a _ ↦ ?_ + refine sum_congr rfl fun b _ ↦ ?_ simp only [mul_pow, prod_mul_distrib, @sum_comm _ _ (Fin n → ℝ), ←mul_sum, ←sum_mul] - refine' sum_congr rfl fun k _ ↦ _ + refine sum_congr rfl fun k _ ↦ ?_ rw [←mul_assoc, mul_right_comm] private lemma step_four {k : Fin n → ℕ} : @@ -106,7 +106,7 @@ private lemma step_four {k : Fin n → ℕ} : rw [piFinsetConst, this, ←Fintype.prod_boole] have : (2 : ℝ) ^ n = ∏ i : Fin n, 2 := by simp rw [this, ←prod_mul_distrib] - refine' prod_congr rfl fun t _ ↦ _ + refine prod_congr rfl fun t _ ↦ ?_ rw [sum_pair, one_pow, mul_boole] swap · norm_num @@ -125,23 +125,23 @@ private lemma step_six {f : G → ℝ} {a b : Fin n → G} : convert sum_le_sum fun k hk ↦ _ rw [mem_piAntidiag] at hk simp only [←mul_assoc, pow_mul] - refine' mul_le_mul_of_nonneg_right _ (prod_nonneg fun i _ ↦ by positivity) + refine mul_le_mul_of_nonneg_right ?_ (prod_nonneg fun i _ ↦ by positivity) norm_cast - refine' double_multinomial.trans _ + refine double_multinomial.trans ?_ rw [hk.1] private lemma step_seven {f : G → ℝ} {a b : Fin n → G} : m ^ m * (∑ i : Fin n, (f (a i) - f (b i)) ^ 2 : ℝ) ^ m ≤ m ^ m * 2 ^ m * (∑ i : Fin n, (f (a i) ^ 2 + f (b i) ^ 2)) ^ m := by rw [←mul_pow, ←mul_pow, ←mul_pow] - refine' pow_le_pow_left _ _ _ + refine pow_le_pow_left ?_ ?_ _ · positivity rw [mul_assoc] - refine' mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _) + refine mul_le_mul_of_nonneg_left ?_ (Nat.cast_nonneg _) rw [mul_sum] - refine' sum_le_sum fun i _ ↦ _ + refine sum_le_sum fun i _ ↦ ?_ rw [sub_eq_add_neg] - refine' add_sq_le.trans_eq _ + refine add_sq_le.trans_eq ?_ simp private lemma step_eight {f : G → ℝ} {a b : Fin n → G} : @@ -149,9 +149,9 @@ private lemma step_eight {f : G → ℝ} {a b : Fin n → G} : m ^ m * 2 ^ (m + (m - 1)) * ((∑ i : Fin n, f (a i) ^ 2) ^ m + (∑ i : Fin n, f (b i) ^ 2) ^ m) := by rw [pow_add, ←mul_assoc _ _ (2 ^ _), mul_assoc _ (2 ^ (m - 1))] - refine' mul_le_mul_of_nonneg_left _ (by positivity) + refine mul_le_mul_of_nonneg_left ?_ (by positivity) rw [sum_add_distrib] - refine' add_pow_le _ _ m <;> positivity + refine add_pow_le ?_ ?_ m <;> positivity private lemma end_step {f : G → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) : (∑ a in A^^n, ∑ b in A^^n, ∑ k : Fin n → ℕ in piAntidiag univ m, @@ -186,7 +186,7 @@ lemma basic_marcinkiewicz_zygmund (f : G → ℝ) (hf : ∀ i : Fin n, ∑ a in · cases m <;> simp · rw [piFinsetConst, piFinset_empty, Finset.sum_empty] cases m <;> simp - refine' (sum_le_sum fun a (_ : a ∈ A^^n) ↦ @step_one' _ _ _ _ hA f hf a).trans _ + refine (sum_le_sum fun a (_ : a ∈ A^^n) ↦ @step_one' _ _ _ _ hA f hf a).trans ?_ rw [←sum_div] simp only [pow_mul, sq_abs] simp only [←pow_mul] @@ -208,12 +208,12 @@ lemma other_marcinkiewicz_zygmund (f : G → ℝ) (hm : m ≠ 0) · simp at hm obtain rfl | hn := n.eq_zero_or_pos · simp - refine' (basic_marcinkiewicz_zygmund f hf).trans _ + refine (basic_marcinkiewicz_zygmund f hf).trans ?_ rw [mul_assoc] - refine' mul_le_mul_of_nonneg_left _ (by positivity) + refine mul_le_mul_of_nonneg_left ?_ (by positivity) rw [Nat.succ_sub_one] simp only [pow_mul, mul_sum] - refine' sum_le_sum fun a _ ↦ _ + refine sum_le_sum fun a _ ↦ ?_ rw [←mul_sum, ←div_le_iff'] have := Real.pow_sum_div_card_le_sum_pow (f := fun i ↦ |f (a i)| ^ 2) univ m fun i _ ↦ ?_ simpa only [Finset.card_fin] using this @@ -250,17 +250,17 @@ lemma complex_marcinkiewicz_zygmund (f : G → ℂ) (hm : m ≠ 0) · exact sum_le_sum fun a _ ↦ add_pow_le (sq_nonneg _) (sq_nonneg _) m · simp only [mul_sum, pow_mul] · rw [mul_assoc, mul_assoc, sum_add_distrib] - refine' mul_le_mul_of_nonneg_left _ _ + refine mul_le_mul_of_nonneg_left ?_ ?_ swap · positivity simp only [sum_add_distrib, mul_add, ←mul_assoc] exact add_le_add h₁ h₂ simp only [mul_sum] - refine' sum_le_sum fun a _ ↦ _ - refine' sum_le_sum fun i _ ↦ _ + refine sum_le_sum fun a _ ↦ ?_ + refine sum_le_sum fun i _ ↦ ?_ rw [pow_mul, pow_mul] - refine' (mul_le_mul_of_nonneg_left (pow_add_pow_le' (sq_nonneg (f (a i)).re) $ - sq_nonneg (f (a i)).im) _).trans_eq _ + refine (mul_le_mul_of_nonneg_left (pow_add_pow_le' (sq_nonneg (f (a i)).re) $ + sq_nonneg (f (a i)).im) ?_).trans_eq ?_ · positivity rw [mul_assoc (2 ^ _ : ℝ), mul_mul_mul_comm, ←_root_.pow_succ, Nat.sub_add_cancel, ←mul_assoc, ←mul_assoc, ←mul_pow, ←mul_assoc] diff --git a/LeanAPAP/Prereqs/Multinomial.lean b/LeanAPAP/Prereqs/Multinomial.lean index e113bc3eb5..ca81a990d5 100644 --- a/LeanAPAP/Prereqs/Multinomial.lean +++ b/LeanAPAP/Prereqs/Multinomial.lean @@ -24,15 +24,15 @@ lemma multinomial_expansion' {α β : Type*} [DecidableEq α] [CommSemiring β] suffices ∀ p : ℕ × ℕ, p ∈ antidiagonal n → ∑ f in piAntidiag s p.2, ((f a + p.1 + s.sum f).choose (f a + p.1) : β) * multinomial s (f + fun t ↦ ite (t = a) p.1 0) * - (x a ^ (f a + p.1) * ∏ t : α in s, x t ^ (f t + ite (t = a) p.1 0)) = - ∑ f in piAntidiag s p.2, n.choose p.1 * multinomial s f * (x a ^ p.1 * ∏ t : α in s, x t ^ f t) by + (x a ^ (f a + p.1) * ∏ t in s, x t ^ (f t + ite (t = a) p.1 0)) = + ∑ f in piAntidiag s p.2, n.choose p.1 * multinomial s f * (x a ^ p.1 * ∏ t in s, x t ^ f t) by rw [sum_congr rfl this] simp only [Nat.antidiagonal_eq_map, sum_map, Function.Embedding.coeFn_mk] rw [add_pow] simp only [ih, sum_mul, mul_sum] - refine' sum_congr rfl fun i _ ↦ sum_congr rfl fun f _ ↦ _ + refine sum_congr rfl fun i _ ↦ sum_congr rfl fun f _ ↦ ?_ ac_rfl - refine' fun p hp ↦ sum_congr rfl fun f hf ↦ _ + refine fun p hp ↦ sum_congr rfl fun f hf ↦ ?_ rw [mem_piAntidiag] at hf rw [not_imp_comm.1 (hf.2 _) has, zero_add, hf.1] congr 2 @@ -41,23 +41,23 @@ lemma multinomial_expansion' {α β : Type*} [DecidableEq α] [CommSemiring β] intro t ht rw [Pi.add_apply, if_neg, add_zero] exact ne_of_mem_of_not_mem ht has - refine' prod_congr rfl fun t ht ↦ _ + refine prod_congr rfl fun t ht ↦ ?_ rw [if_neg, add_zero] exact ne_of_mem_of_not_mem ht has lemma double_multinomial : (multinomial s fun i ↦ 2 * f i) ≤ ((∑ i in s, f i) ^ ∑ i in s, f i) * multinomial s f := by rw [multinomial, multinomial, ←mul_sum] - refine' Nat.div_le_of_le_mul' _ + refine Nat.div_le_of_le_mul' ?_ rw [←mul_assoc, ←Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _), Nat.le_div_iff_mul_le] swap · exact prod_pos fun i _ ↦ by positivity - refine' (Nat.mul_le_mul_right _ $ factorial_two_mul_le _).trans _ + refine (Nat.mul_le_mul_right _ $ factorial_two_mul_le _).trans ?_ rw [mul_pow, mul_comm, ←mul_assoc, ←mul_assoc] - refine' Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ _) + refine Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ ?_) rw [←Finset.prod_pow_eq_pow_sum, ←prod_mul_distrib] - refine' prod_le_prod' fun i _ ↦ _ + refine prod_le_prod' fun i _ ↦ ?_ rw [mul_comm, ←doubleFactorial_two_mul] exact doubleFactorial_le_factorial _ diff --git a/LeanAPAP/Prereqs/WideDiag.lean b/LeanAPAP/Prereqs/WideDiag.lean deleted file mode 100644 index adb9d1cfbd..0000000000 --- a/LeanAPAP/Prereqs/WideDiag.lean +++ /dev/null @@ -1,62 +0,0 @@ -import Mathlib.Data.Finset.Pointwise - -/-! -# Wide diagonal --/ - -open scoped Pointwise - -namespace Finset -variable {α : Type*} [DecidableEq α] {s : Finset α} {k : ℕ} - -def wideDiag (k : ℕ) (s : Finset α) : Finset (Fin k → α) := s.image fun i _ ↦ i - -lemma mem_wideDiag {k : ℕ} {x : Fin k → α} : - x ∈ s.wideDiag k ↔ ∃ i ∈ s, (fun _ ↦ i) = x := mem_image - -def fintypeWideDiag (α : Type*) [DecidableEq α] [Fintype α] (k : ℕ) : Finset (Fin k → α) := - univ.wideDiag k - -lemma mem_fintypeWideDiag [Fintype α] {k : ℕ} {x : Fin k → α} : - x ∈ fintypeWideDiag α k ↔ ∃ i, (fun _ ↦ i) = x := - mem_wideDiag.trans (by simp) - -@[simp] lemma card_wideDiag (hk : k ≠ 0) (s : Finset α) : (s.wideDiag k).card = s.card := by - cases k - · cases hk rfl - rw [Finset.wideDiag, card_image_of_injective] - exact fun i j h ↦ congr_fun h 0 - -section Add -variable [Add α] - -lemma big_shifts_step1 (L : Finset (Fin k → α)) (hk : k ≠ 0) : - ∑ x in L + s.wideDiag k, ∑ l in L, ∑ s in s.wideDiag k, (if l + s = x then 1 else 0) - = L.card * s.card := by - simp only [@sum_comm _ _ _ _ (L + _), sum_ite_eq] - rw [sum_const_nat] - intro l hl - rw [sum_const_nat, mul_one, Finset.card_wideDiag hk] - exact fun s hs ↦ if_pos (Finset.add_mem_add hl hs) - -end Add - -variable [AddCommGroup α] [Fintype α] - -lemma reindex_count (L : Finset (Fin k → α)) (hk : k ≠ 0) (hL' : L.Nonempty) (l₁ : Fin k → α) : - ∑ l₂ in L, ite (l₁ - l₂ ∈ fintypeWideDiag α k) 1 0 = - (univ.filter fun t ↦ (l₁ - fun _ ↦ t) ∈ L).card := - calc - ∑ l₂ : Fin k → α in L, ite (l₁ - l₂ ∈ fintypeWideDiag α k) 1 0 = - ∑ l₂ in L, ∑ t : α, ite ((l₁ - fun _ ↦ t) = l₂) 1 0 := by - refine' sum_congr rfl fun l₂ hl₂ ↦ _ - rw [Fintype.sum_ite_eq_ite_exists] - simp only [mem_fintypeWideDiag, @eq_comm _ l₁, eq_sub_iff_add_eq, sub_eq_iff_eq_add'] - rintro i j h rfl - cases k - · simp at hk - · simpa using congr_fun h 0 - _ = (univ.filter fun t ↦ (l₁ - fun _ ↦ t) ∈ L).card := by - simp only [sum_comm, sum_ite_eq, card_eq_sum_ones, sum_filter] - -end Finset diff --git a/lake-manifest.json b/lake-manifest.json index 9dc6d61d70..0c03dce49c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239", + "rev": "ac82ca1064a77eb76d37ae2ab2d1cdeb942d57fe", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "27990300a94dd6789254c2ffef4023896d3717c6", + "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d419680bd7d6378744b29e71e3e161a996e82178", + "rev": "70d37777965d3605c1c421a727e3cea932d0370e", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -85,17 +85,27 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c74a052aebee847780e165611099854de050adf7", + "rev": "f93115d0209de6db335725dee900d379f40c0317", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "", - "rev": "194403be8599ce1d95afa15113960045f8483c7c", + "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main",