AlmostPeriodicity.linfty_almost_periodicity

public theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hK₂ : 2 ≤ K)    (hK : σ[A, S] ≤ K) (B C : Finset G) (hB : B.Nonempty) (hC : C.Nonempty) :    ∃ T : Finset G,      K ^ (-4096 * ⌈𝓛 (#C / #B)⌉ / ε ^ 2) * #S ≤ #T ∧      ∀ t ∈ T, ‖τ t (μ_[ℂ] A ∗ᵈ 𝟭_[B] ∗ᵈ μ C) - μ A ∗ᵈ 𝟭_[B] ∗ᵈ μ C‖_[∞] ≤ ε := by  let r : ℝ := min 1 (#C / #B)  set m : ℝ := 𝓛 (#C / #B)  have hm₀ : 0 < m := curlog_pos (by positivity)  have hm₁ : 1 ≤ ⌈m⌉₊ := Nat.one_le_iff_ne_zero.2 <| by positivity  obtain ⟨T, hKT, hT⟩ := almost_periodicity (ε / exp 1) (by positivity)    (div_le_one_of_le₀ (hε₁.trans <| one_le_exp zero_le_one) <| by positivity) ⌈m⌉₊ (𝟭_[B]) hK₂ hK  norm_cast at hT  set M : ℕ := 2 * ⌈m⌉₊  have hM₀ : (M : ℝ≥0) ≠ 0 := by positivity  have hM₁ : 1 < (M : ℝ≥0) := by norm_cast; simp [← Nat.succ_le_iff, M]; linarith  have hM : (M : ℝ≥0).HolderConjugate _ := NNReal.HolderConjugate.conjExponent hM₁  have : (M : ℝ≥0∞).HolderConjugate _ := hM.coe_ennreal  refine ⟨T, ?_, fun t ht ↦ ?_⟩  · calc      _ = K ^(-(512 * 8) / ε ^ 2 * ⌈m⌉₊) * #S := by          rw [mul_div_right_comm, natCast_ceil_eq_intCast_ceil hm₀.le]; norm_num      _ ≤ K ^(-(512 * exp 1 ^ 2) / ε ^ 2 * ⌈m⌉₊) * #S := by          gcongr          · exact one_le_two.trans hK₂          calc            _ ≤ (2.7182818286 : ℝ) ^ 2 := by gcongr; exact exp_one_lt_d9.le            _ ≤ _ := by norm_num      _ = _ := by simp [div_div_eq_mul_div, ← mul_div_right_comm, mul_right_comm, div_pow]      _ ≤ _ := hKT  set F : G → ℂ := τ t (μ A ∗ᵈ 𝟭_[B]) - μ A ∗ᵈ 𝟭_[B]  have (x : G) :=    calc      (τ t (μ A ∗ᵈ 𝟭_[B] ∗ᵈ μ C) - μ A ∗ᵈ 𝟭_[B] ∗ᵈ μ C : G → ℂ) x        = (F ∗ᵈ μ C) x := by simp [sub_ddconv, F]      _ = ∑ y, F y * μ C (x - y) := ddconv_eq_sum_sub' ..      _ = ∑ y, F y * μ (x +ᵥ -C) y := by simp [neg_add_eq_sub]  rw [MeasureTheory.dLinftyNorm_eq_iSup_norm]  refine ciSup_le fun x ↦ ?_  calc    ‖(τ t (μ A ∗ᵈ 𝟭_[B] ∗ᵈ μ C) - μ A ∗ᵈ 𝟭_[B] ∗ᵈ μ C : G → ℂ) x‖      = ‖∑ y, F y * μ (x +ᵥ -C) y‖ := by rw [this]    _ ≤ ∑ y, ‖F y * μ (x +ᵥ -C) y‖ := norm_sum_le _ _    _ = ‖F * μ (x +ᵥ -C)‖_[1] := by rw [MeasureTheory.dL1Norm_eq_sum_norm]; rfl    _ ≤ ‖F‖_[M] * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := MeasureTheory.dLpNorm_mul_le  _ _    _ ≤ ε / exp 1 * #B ^ (M : ℝ)⁻¹ * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := by        gcongr        simpa [← ENNReal.coe_natCast, MeasureTheory.dLpNorm_indicator_one hM₀, F] using hT _ ht    _ = ε * ((#C / #B) ^ (-(M : ℝ)⁻¹) / exp 1) := by        rw [← mul_comm_div, MeasureTheory.dLpNorm_mu hM.symm.lt.le hC.neg.vadd_finset,          card_vadd_finset, card_neg, hM.symm.coe.inv_sub_one, div_rpow, mul_assoc]        any_goals positivity        push_cast        rw [rpow_neg, rpow_neg, ← div_eq_mul_inv, inv_div_inv]        all_goals positivity    _ ≤ ε := mul_le_of_le_one_right (by positivity) <| (div_le_one <| by positivity).2 ?_  calc    (#C / #B : ℝ) ^ (-(M : ℝ)⁻¹)      ≤ r ^ (-(M : ℝ)⁻¹) :=        rpow_le_rpow_of_nonpos (by positivity) inf_le_right <| neg_nonpos.2 <| by positivity    _ ≤ r ^ (-(1 + log r⁻¹)⁻¹) :=        rpow_le_rpow_of_exponent_ge (by positivity) inf_le_left <| neg_le_neg <| inv_anti₀          (by positivity) <| (Nat.le_ceil _).trans <|            mod_cast Nat.le_mul_of_pos_left _ (by positivity)    _ ≤ r ^ (-(0 + log r⁻¹)⁻¹) := by      obtain hr | hr : r = 1 ∨ r < 1 := inf_le_left.eq_or_lt      · simp [hr]      have : 0 < log r⁻¹ := log_pos <| (one_lt_inv₀ (by positivity)).2 hr      exact rpow_le_rpow_of_exponent_ge (by positivity) inf_le_left (by gcongr; exact zero_le_one)    _ = r ^ (log r)⁻¹ := by simp [inv_neg]    _ ≤ exp 1 := rpow_inv_log_le_exp_one