AlmostPeriodicity.linfty_almost_periodicity_boosted

public theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (k : ℕ)    (hk : k ≠ 0) (hK₂ : 2 ≤ K) (hK : σ[A, S] ≤ K) (hS : S.Nonempty)    (B C : Finset G) (hB : B.Nonempty) (hC : C.Nonempty) :    ∃ T : Finset G,      K ^ (-4096 * ⌈𝓛 (#C / #B)⌉ * k ^ 2/ ε ^ 2) * #S ≤ #T ∧      ‖μ T ∗ᵈ^ k ∗ᵈ (μ_[ℂ] A ∗ᵈ 𝟭_[B] ∗ᵈ μ C) - μ A ∗ᵈ 𝟭_[B] ∗ᵈ μ C‖_[∞] ≤ ε := by  obtain ⟨T, hKT, hT⟩ := linfty_almost_periodicity (ε / k) (by positivity)    (div_le_one_of_le₀ (hε₁.trans <| mod_cast Nat.one_le_iff_ne_zero.2 hk) <| by positivity) hK₂ hK    _ _ hB hC  refine ⟨T, by simpa only [div_pow, div_div_eq_mul_div] using hKT, ?_⟩  set F := μ_[ℂ] A ∗ᵈ 𝟭_[B] ∗ᵈ μ C  have hT' : T.Nonempty := by    have : (0 : ℝ) < #T := hKT.trans_lt' <| by positivity    simpa [card_pos] using this  calc    (‖μ T ∗ᵈ^ k ∗ᵈ F - F‖_[∞] : ℝ)      = ‖𝔼 a ∈ T ^^ k, (τ (∑ i, a i) F - F)‖_[∞] := by        rw [mu_iterConv_ddconv, expect_sub_distrib, expect_const hT'.piFinset_const]    _ ≤ 𝔼 a ∈ T ^^ k, ‖τ (∑ i, a i) F - F‖_[∞] := MeasureTheory.dLpNorm_expect_le le_top    _ ≤ 𝔼 _a ∈ T ^^ k, ε := ?_    _ = ε := by rw [expect_const hT'.piFinset_const]  refine expect_le_expect fun x hx ↦  calc    (‖τ (∑ i, x i) F - F‖_[⊤] : ℝ)    _ ≤ ∑ i, ‖τ (x i) F - F‖_[⊤] := MeasureTheory.dLpNorm_translate_sum_sub_le le_top _ _ _    _ ≤ ∑ _i, ε / k := by gcongr; exact hT _ <| Fintype.mem_piFinset.1 hx _    _ = ε := by simp only [sum_const, card_fin, nsmul_eq_mul]; rw [mul_div_cancel₀]; positivity