finish fixing!

LeanAPAP/Mathlib/Data/Finset/Card.lean

@@ -1,5 +1,7 @@
 import Mathlib.Data.Finset.Card
 
+attribute [pp_dot] Finset.card
+
 namespace Finset
 variable {α R : Type*} [AddGroupWithOne R] [DecidableEq α] {s t : Finset α}
 

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -52,8 +52,8 @@ open Finset
 open scoped BigOperators Pointwise
 
 lemma big_shifts_step1 (L : Finset (Fin k → G)) (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
+    ∑ 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

LeanAPAP/Physics/DRC.lean

@@ -50,9 +50,9 @@ private lemma sum_cast_c (p : ℕ) (B A : Finset G) :
 private lemma lpNorm_conv_pos (hp : p ≠ 0) (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty) :
     0 < ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p := by
   rw [wlpNorm_pow_eq_sum]
-  refine' sum_pos' (fun x _ ↦ smul_nonneg zero_le' $ by positivity)
-      ⟨0, mem_univ _, smul_pos _ $ pow_pos _ _⟩
-  · refine' lt_of_le_of_ne' (Pi.le_def.1 (dconv_nonneg mu_nonneg mu_nonneg) _) _
+  refine sum_pos' (fun x _ ↦ smul_nonneg zero_le' $ by positivity)
+      ⟨0, mem_univ _, smul_pos ?_ $ pow_pos ?_ _⟩
+  · refine lt_of_le_of_ne' (Pi.le_def.1 (dconv_nonneg mu_nonneg mu_nonneg) _) ?_
     rwa [←Function.mem_support, support_dconv, support_mu, support_mu, ←coe_sub, mem_coe,
       zero_mem_sub_iff, not_disjoint_iff_nonempty_inter] <;>
       exact mu_nonneg
@@ -65,7 +65,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty) :
     ∃ A₁, A₁ ⊆ B₁ ∧ ∃ A₂, A₂ ⊆ B₂ ∧
       ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ f⟫_[ℝ] * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p
-        ≤ 2 * ∑ x, (μ B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x ∧
+        ≤ 2 * ∑ x, (μ B₁ ○ μ B₂) x * (𝟭_[ℝ] A ○ 𝟭 A) x ^ p * f x ∧
       (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p)
         ≤ A₁.card / B₁.card ∧
       (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p)
@@ -81,25 +81,25 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
   have hM : 0 < M := by rw [hM_def]; positivity
   replace hf : 0 < ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x
   · have : 0 ≤ μ_[ℝ] B₁ ○ μ B₂ * (𝟭 A ○ 𝟭 A) ^ p * (↑) ∘ f := sorry -- positivity
-    refine' Fintype.sum_pos $ this.gt_iff_ne.2 $ support_nonempty_iff.1 _
+    refine Fintype.sum_pos $ this.gt_iff_ne.2 $ support_nonempty_iff.1 ?_
     simp only [support_comp_eq, Set.Nonempty, and_assoc, support_mul', support_dconv,
       indicate_nonneg, mu_nonneg, support_indicate, support_mu, NNReal.coe_eq_zero, iff_self_iff,
       forall_const, Set.mem_inter_iff, ←coe_sub, mem_coe, support_pow _ hp₀, hf]
   set A₁ := fun s ↦ B₁ ∩ c p A s
   set A₂ := fun s ↦ B₂ ∩ c p A s
   set g : (Fin p → G) → ℝ := fun s ↦ (A₁ s).card * (A₂ s).card with hg_def
-  have hg : ∀ s, 0 ≤ g s := fun s ↦ by rw [hg_def] <;> dsimp <;> positivity
+  have hg : ∀ s, 0 ≤ g s := fun s ↦ by rw [hg_def]; dsimp; positivity
   have hgB : ∑ s, g s = B₁.card * B₂.card * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p := by
     have hAdconv : 0 ≤ 𝟭_[ℝ] A ○ 𝟭 A := dconv_nonneg indicate_nonneg indicate_nonneg
     simpa only [wlpNorm_pow_eq_sum hp₀, l2inner_eq_sum, sum_dconv, sum_indicate, Pi.one_apply,
       IsROrC.inner_apply, IsROrC.conj_to_real, norm_of_nonneg (hAdconv _), mul_one, nsmul_eq_mul,
       Nat.cast_mul, ←hg_def, NNReal.smul_def, NNReal.coe_dconv, NNReal.coe_comp_mu]
         using lemma_0 p B₁ B₂ A 1
   suffices : ∑ s, ⟪𝟭_[ℝ] (A₁ s) ○ 𝟭 (A₂ s), (↑) ∘ f⟫_[ℝ] * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p
-    < ∑ s, 𝟭 (univ.filter fun s ↦ M ^ 2 ≤ g s) s * g s * 2 *
-      ∑ x, (μ B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x
+    < ∑ s, 𝟭 (univ.filter fun s ↦ M ^ 2 ≤ g s) s * g s *
+        (2 * ∑ x, (μ B₁ ○ μ B₂) x * (𝟭_[ℝ] A ○ 𝟭 A) x ^ p * f x)
   · obtain ⟨s, -, hs⟩ := exists_lt_of_sum_lt this
-    refine' ⟨_, inter_subset_left _ $ c p A s, _, inter_subset_left _ $ c p A s, _⟩
+    refine ⟨_, inter_subset_left _ $ c p A s, _, inter_subset_left _ $ c p A s, ?_⟩
     simp only [indicate_apply, mem_filter, mem_univ, true_and_iff, boole_mul] at hs
     split_ifs at hs with h; swap
     · simp only [MulZeroClass.zero_mul, l2inner_eq_sum, Function.comp_apply, IsROrC.inner_apply,
@@ -113,44 +113,46 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
       simpa [hg_def, hM_def, mul_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num,
         mul_div_right_comm] using h
       positivity
-    refine' ⟨lt_of_mul_lt_mul_left (hs.trans_eq' _) (hg s), this.trans $ mul_le_of_le_one_right _ $
-      div_le_one_of_le _ _, this.trans $ mul_le_of_le_one_left _ $ div_le_one_of_le _ _⟩
-    · simp_rw [←card_smul_mu, smul_dconv, dconv_smul, l2inner_smul_left, star_trivial, hg_def,
-      nsmul_eq_mul, mul_assoc]
+    refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) $ hg s).le, this.trans $ mul_le_of_le_one_right
+      ?_ $ div_le_one_of_le ?_ ?_, this.trans $ mul_le_of_le_one_left ?_ $ div_le_one_of_le ?_ ?_⟩
+    · simp_rw [←card_smul_mu, smul_dconv, dconv_smul, l2inner_smul_left, star_trivial, nsmul_eq_mul,
+         mul_assoc]
     any_goals positivity
     all_goals exact Nat.cast_le.2 $ card_mono $ inter_subset_left _ _
   rw [←sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ←sum_mul, mul_right_comm, ←hgB, mul_left_comm,
     ←mul_assoc]
   simp only [indicate_apply, boole_mul, mem_filter, mem_univ, true_and_iff, ←sum_filter,
     mul_lt_mul_right hf, Function.comp_apply]
   by_cases h : ∀ s, g s ≠ 0 → M ^ 2 ≤ g s
-  · rw [←@sum_filter_ne_zero _ _ Filter _ _, Finset.filter_comm,
-      filter_true_of_mem fun s hs ↦ h s mem_filter.1 hs.2, ←sum_filter_ne_zero]
-    refine' lt_mul_of_one_lt_left
-      (sum_pos fun s hs ↦ h _ mem_filter.1 hs.2.trans_lt' $ by positivity _) one_lt_two
+  · rw [←@sum_filter_ne_zero _ _ (filter _ _), Finset.filter_comm,
+      filter_true_of_mem fun s hs ↦ h s (mem_filter.1 hs).2, ←sum_filter_ne_zero]
+    refine lt_mul_of_one_lt_left (sum_pos (fun s hs ↦ (h _ (mem_filter.1 hs).2).trans_lt' $
+      by positivity) ?_) one_lt_two
     rw [←sum_filter_ne_zero] at hgB
-    exact nonempty_of_sum_ne_zero hgB.trans_ne $ by positivity
+    exact nonempty_of_sum_ne_zero $ hgB.trans_ne $ by positivity
   push_neg at h
   obtain ⟨s, hs⟩ := h
   suffices h : (2 : ℝ) * ∑ s with g s < M ^ 2, g s < ∑ s, g s
-  · refine' le_or_lt_of_add_le_add _.resolve_left h.not_le
+  · refine (le_or_lt_of_add_le_add ?_).resolve_left h.not_le
     simp_rw [←not_le, ←compl_filter, ←two_mul, ←mul_add, sum_compl_add_sum]
-  rw [←lt_div_iff' zero_lt_two' ℝ, div_eq_inv_mul]
+    rfl
+  rw [←lt_div_iff' (zero_lt_two' ℝ), div_eq_inv_mul]
   calc
-    ∑ s with g s < M ^ 2, g s = ∑ s with g s < M ^ 2 ∧ g s ≠ 0, sqrt g s * sqrt g s
-          := by simp_rw [mul_self_sqrt hg _, ←filter_filter, sum_filter_ne_zero]
-      _ < ∑ s with g s < M ^ 2 ∧ g s ≠ 0, M * sqrt g s
-          := sum_lt_sum_of_nonempty ⟨s, mem_filter.2 ⟨mem_univ _, hs.symm⟩⟩ _
-      _ ≤ ∑ s, M * sqrt g s := sum_le_univ_sum_of_nonneg fun s ↦ by positivity
-      _ = M * ∑ s, sqrt (A₁ s).card * sqrt (A₂ s).card
-          := by simp_rw [mul_sum, sqrt_mul Nat.cast_nonneg _]
-      _ ≤ M * sqrt (∑ s, (A₁ s).card) * sqrt (∑ s, (A₂ s).card)
+    ∑ s with g s < M ^ 2, g s = ∑ s with g s < M ^ 2 ∧ g s ≠ 0, sqrt (g s) * sqrt (g s)
+          := by simp_rw [mul_self_sqrt (hg _), ←filter_filter, sum_filter_ne_zero]
+      _ < ∑ s with g s < M ^ 2 ∧ g s ≠ 0, M * sqrt (g s)
+          := sum_lt_sum_of_nonempty ⟨s, mem_filter.2 ⟨mem_univ _, hs.symm⟩⟩ ?_
+      _ ≤ ∑ s, M * sqrt (g s) := sum_le_univ_sum_of_nonneg fun s ↦ by positivity
+      _ = M * (∑ s, sqrt (A₁ s).card * sqrt (A₂ s).card)
+          := by simp_rw [mul_sum, sqrt_mul $ Nat.cast_nonneg _]
+      _ ≤ M * (sqrt (∑ s, (A₁ s).card) * sqrt (∑ s, (A₂ s).card))
           := mul_le_mul_of_nonneg_left
-            sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity hM.le
-      _ = _ := _
+            (sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity) hM.le
+      _ = _ := ?_
   · simp only [mem_filter, mem_univ, true_and_iff, Nat.cast_nonneg, and_imp]
-    exact fun s hsM hs ↦ mul_lt_mul_of_pos_right sqrt_lt' hM.2 hsM sqrt_pos.2 $ hg _.lt_of_ne' hs
-  rw [sum_cast_c, sum_cast_c, sqrt_mul', sqrt_mul', mul_mul_mul_comm sqrt _, mul_self_sqrt,
+    exact fun s hsM hs ↦ mul_lt_mul_of_pos_right ((sqrt_lt' hM).2 hsM) $
+      sqrt_pos.2 $ (hg _).lt_of_ne' hs
+  rw [sum_cast_c, sum_cast_c, sqrt_mul', sqrt_mul', mul_mul_mul_comm (sqrt _), mul_self_sqrt,
     ←mul_assoc, hM_def, div_mul_cancel, ←sqrt_mul, mul_assoc, mul_self_sqrt, hgB, mul_right_comm,
     mul_assoc]
   all_goals positivity
@@ -174,7 +176,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
   obtain ⟨A₁, hAB₁, A₂, hAB₂, h, hcard₁, hcard₂⟩ :=
     drc hp₂ (𝟭 (s p ε B₁ B₂ A)ᶜ)
       (by simpa only [support_indicate, coe_compl, Set.mem_compl_iff, mem_coe]) hB hA
-  refine' ⟨A₁, hAB₁, A₂, hAB₂, _, hcard₁, hcard₂⟩
+  refine ⟨A₁, hAB₁, A₂, hAB₂, ?_, hcard₁, hcard₂⟩
   have hp₀ : 0 < p := by positivity
   have aux :
     ∀ (c : Finset G) (r),
@@ -191,32 +193,32 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
   clear hcard₁ hcard₂ aux
   rw [sub_le_comm]
   calc
-    _ = ∑ x in s p ε B₁ B₂ Aᶜ, (μ A₁ ○ μ A₂) x := _
-    _ = ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ 𝟭_[ℝ≥0] (s (↑p) ε B₁ B₂ Aᶜ)⟫_[ℝ] := by
-      simp [l2inner_eq_sum, -mem_compl, -mem_s, apply_ite (↑), indicate_apply]
-    _ ≤ _ := ((le_div_iff $ lpNorm_conv_pos hp₀.ne' hB hA).2 h)
-    _ ≤ _ := _
+    _ = ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ A₁ ○ μ A₂) x := ?_
+    _ = ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ 𝟭_[ℝ≥0] ((s (↑p) ε B₁ B₂ A)ᶜ)⟫_[ℝ] := by
+      simp [l2inner_eq_sum, -mem_compl, -mem_s, apply_ite NNReal.toReal, indicate_apply]
+    _ ≤ _ := (le_div_iff $ lpNorm_conv_pos hp₀.ne' hB hA).2 h
+    _ ≤ _ := ?_
   · simp_rw [sub_eq_iff_eq_add', sum_add_sum_compl, sum_dconv, map_mu]
-    rw [sum_mu _ hA₁, sum_mu _ hA₂, one_mul] <;> infer_instance
+    rw [sum_mu _ hA₁, sum_mu _ hA₂, one_mul]
   rw [div_le_iff (lpNorm_conv_pos hp₀.ne' hB hA), ←le_div_iff' (zero_lt_two' ℝ)]
-  simp only [apply_ite (↑), indicate_apply, Nonneg.coe_one, Nonneg.coe_zero, mul_boole, sum_ite_mem,
-    univ_inter, mul_div_right_comm]
+  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]
   calc
-    ∑ x in s p ε B₁ B₂ Aᶜ, (μ B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p ≤
-        ∑ x in s p ε B₁ B₂ Aᶜ, (μ B₁ ○ μ B₂) x * ((1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂]) ^ p :=
-      sum_le_sum fun x hx ↦
-        mul_le_mul_of_nonneg_left
-          (pow_le_pow_of_le_left (dconv_nonneg indicate_nonneg indicate_nonneg _)
-            (by simpa using hx) _)
+    ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p ≤
+        ∑ x in (s p ε B₁ B₂ A)ᶜ,
+          (μ B₁ ○ μ B₂) x * ((1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂]) ^ p :=
+      sum_le_sum fun x hx ↦ mul_le_mul_of_nonneg_left (pow_le_pow_of_le_left
+        (dconv_nonneg indicate_nonneg indicate_nonneg _) (by simpa using hx) _)
           (dconv_nonneg mu_nonneg mu_nonneg _)
     _ ≤ ∑ x, (μ B₁ ○ μ B₂) x * ((1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂]) ^ p :=
       (sum_le_univ_sum_of_nonneg fun x ↦
         mul_nonneg (dconv_nonneg mu_nonneg mu_nonneg _) $ hp.pow_nonneg _)
-    _ = ‖μ_[ℝ] B₁‖_[1] * ‖μ_[ℝ] B₂‖_[1] * ((1 - ε) ^ p * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p) := _
+    _ = ‖μ_[ℝ] B₁‖_[1] * ‖μ_[ℝ] B₂‖_[1] * ((1 - ε) ^ p * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p)
+        := ?_
     _ ≤ _ :=
       (mul_le_of_le_one_left (mul_nonneg (hp.pow_nonneg _) $ hp.pow_nonneg _) $
         mul_le_one L1norm_mu_le_one lpNorm_nonneg L1norm_mu_le_one)
-    _ ≤ _ := mul_le_mul_of_nonneg_right _ $ hp.pow_nonneg _
+    _ ≤ _ := mul_le_mul_of_nonneg_right ?_ $ hp.pow_nonneg _
   · have : 0 ≤ μ_[ℝ] B₁ ○ μ B₂ := dconv_nonneg mu_nonneg mu_nonneg
     simp_rw [←L1norm_dconv mu_nonneg mu_nonneg, L1norm_eq_sum, norm_of_nonneg (this _), sum_mul,
       mul_pow]
@@ -225,7 +227,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
     _ = exp (-(ε * p)) := by rw [←neg_mul, exp_mul, rpow_nat_cast]
     _ ≤ exp (-log (2 / δ)) :=
       (exp_monotone $ neg_le_neg $ (inv_mul_le_iff $ by positivity).1 hpε)
-    _ = δ / 2 := by rw [exp_neg, exp_log, inv_div] <;> positivity
+    _ = δ / 2 := by rw [exp_neg, exp_log, inv_div]; positivity
 
 --TODO: When `1 < ε`, the result is trivial since `S = univ`.
 /-- Special case of `sifting` when `B₁ = B₂ = univ`. -/