Get rid of dilate for now

LeanAPAP.lean

@@ -2,6 +2,7 @@ import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import LeanAPAP.Mathlib.Order.LiminfLimsup
 import LeanAPAP.Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.Probability.UniformOn
 import LeanAPAP.Mathlib.Tactic.Positivity
@@ -22,7 +23,6 @@ import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.FourierTransform.Convolution
 import LeanAPAP.Prereqs.FourierTransform.Discrete
-import LeanAPAP.Prereqs.Function.Dilate
 import LeanAPAP.Prereqs.Function.Indicator.Basic
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs

LeanAPAP/Prereqs/FourierTransform/Compact.lean

@@ -106,13 +106,6 @@ lemma cft_conjneg (f : α → ℂ) : cft (conjneg f) = conj (cft f) := funext $
 @[simp] lemma cft_balance (f : α → ℂ) (hψ : ψ ≠ 0) : cft (balance f) ψ = cft f ψ := by
   simp only [balance, Pi.sub_apply, cft_sub, cft_const _ hψ, sub_zero]
 
-lemma cft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime n) :
-    cft (dilate f n) ψ = cft f (ψ ^ n) := by
-  simp_rw [cft_apply, wInner_cWeight_eq_expect, dilate]
-  rw [← Nat.card_eq_fintype_card] at hn
-  refine (Fintype.expect_bijective _ hn.nsmul_right_bijective _ _  ?_).symm
-  simp only [pow_apply, ← map_nsmul_eq_pow, zmod_val_inv_nsmul_nsmul hn, forall_const]
-
 @[simp] lemma cft_trivNChar [DecidableEq α] : cft (trivNChar : α → ℂ) = 1 := by
   ext
   simp [trivChar_apply, cft_apply, wInner_cWeight_eq_expect, ← map_expect, card_univ, NNRat.smul_def]

LeanAPAP/Prereqs/FourierTransform/Discrete.lean

@@ -2,7 +2,6 @@ import Mathlib.Algebra.BigOperators.Balance
 import Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
 import Mathlib.MeasureTheory.Constructions.AddChar
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
-import LeanAPAP.Prereqs.Function.Dilate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Inner.Hoelder.Compact
 
@@ -105,13 +104,6 @@ lemma dft_comp_neg_apply (f : α → ℂ) (ψ : AddChar α ℂ) :
 @[simp] lemma dft_balance (f : α → ℂ) (hψ : ψ ≠ 0) : dft (balance f) ψ = dft f ψ := by
   simp only [balance, Pi.sub_apply, dft_sub, dft_const _ hψ, sub_zero]
 
-lemma dft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime n) :
-    dft (dilate f n) ψ = dft f (ψ ^ n) := by
-  simp_rw [dft_apply, wInner_one_eq_sum, dilate]
-  rw [← Nat.card_eq_fintype_card] at hn
-  refine (Fintype.sum_bijective _ hn.nsmul_right_bijective _ _  ?_).symm
-  simp only [pow_apply, ← map_nsmul_eq_pow, zmod_val_inv_nsmul_nsmul hn, forall_const]
-
 @[simp] lemma dft_trivChar [DecidableEq α] : dft (trivChar : α → ℂ) = 1 := by
   ext; simp [trivChar_apply, dft_apply, wInner_one_eq_sum, ← map_sum]