Di in ff

public lemma di_in_ff [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq : q.Prime)    (hε₀ : 0 < ε) (hε₁ : ε < 1) (hγC : γ ≤ C.dens) (hγ : 0 < γ)    (hAC : ε ≤ |card G * ⟪μ_[ℝ] A ∗ᵈ μ A, μ C⟫_[ℝ] - 1|) :    ∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)),        ↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤            2 ^ 128 * 𝓛 A.dens ^ 4 * 𝓛 γ ^ 4 / ε ^ 12 ∧          (1 + ε / 32) * A.dens ≤ ‖𝟭_[(A : Set G), ℝ] ∗ᵈ μ (Set.toFinset V)‖_[∞] := by  have hγ₁ : γ ≤ 1 := hγC.trans (by norm_cast; exact dens_le_one)  obtain rfl | hA₀ := A.eq_empty_or_nonempty  · refine ⟨⊤, Classical.decPred _, ?_, by simp⟩    simp only [finrank_top, tsub_self, CharP.cast_eq_zero, dens_empty, NNRat.cast_zero, inv_zero,      log_zero, add_zero, one_pow, mul_one]    positivity  have hε₁' : 1 ≤ ε⁻¹ := (one_le_inv₀ hε₀).2 hε₁.le  let α : ℝ := A.dens  have hα₀ : 0 < α := by positivity  have hα₁ : α ≤ 1 := by unfold α; exact mod_cast A.dens_le_one  have : 0 ≤ log γ⁻¹ := log_nonneg <| (one_le_inv₀ hγ).2 hγ₁  have : 0 < 𝓛 γ := curlog_pos hγ.le hγ₁  have : 1 ≤ 𝓛 γ := one_le_curlog hγ.le hγ₁  let p : ℕ := 2 * ⌈𝓛 γ⌉₊  have hpupper : p ≤ 4 * 𝓛 γ := by    unfold p; push_cast; grw [Nat.ceil_le_two_mul (by linarith)]; grind  have : 0 < p := by positivity  let f : G → ℝ := balance (μ A)  obtain ⟨p', hp'upper, unbalancing⟩ :    ∃ p' : ℕ, p' ≤ 2 ^ 10 * (ε / 2)⁻¹ ^ 2 * p ∧      1 + ε / 2 / 2 ≤ ‖card G • (f ○ᵈ f) + 1‖_[p', μ univ] := by    refine unbalancing _ (mul_ne_zero two_ne_zero (Nat.ceil_pos.2 <| curlog_pos hγ.le hγ₁).ne')      (ε / 2) (by positivity) (div_le_one_of_le₀ (hε₁.le.trans <| by norm_num) <| by norm_num)      (card G • (balance (μ A) ○ᵈ balance (μ A))) (sqrt (card G) • balance (μ A)) (μ univ) ?_ ?_ ?_    · ext a : 1      simp [smul_dddconv, dddconv_smul, ← mul_assoc, ← sq, ← Complex.ofReal_pow]    · simp    · have global_dichotomy := global_dichotomy hA₀ hγC hγ hAC      simpa [wLpNorm_nsmul, ← nsmul_eq_mul, div_le_iff₀' (show (0 : ℝ) < card G by positivity),        ← div_div, rpow_neg, inv_rpow] using global_dichotomy  have : 0 < p' := pos_iff_ne_zero.2 <| by rintro rfl; simp at unbalancing; linarith  let q' : ℕ := max (2 * p') (2 ^ 4 * ⌈ε⁻¹ * log (64 / ε)⌉₊)  have : 0 < q' := by positivity  have hq'even : Even q' := by grind  have hp'q' : p' ≤ q' := by unfold q'; grw [← le_max_left]; lia  have hq'lower : 2 ^ 4 * ε⁻¹ * log (64 / ε) ≤ q' := by    unfold q'; grw [mul_assoc, ← le_max_right]; push_cast; grw [← Nat.le_ceil]; norm_num  have hq'upper : q' ≤ 2 ^ 16 * 𝓛 γ / ε ^ 2 := by    unfold q'    push_cast    grw [hp'upper, hpupper, max_le_add_of_nonneg (by positivity) (by positivity),      (64 / ε).log_le_self (by positivity)]    ring_nf    grw [Nat.ceil_le_two_mul <| by grw [← hε₁']; norm_num]    ring_nf    bound  have : 0 < log (6 / ε) := log_pos <| (one_lt_div hε₀).2 (by linarith)  have : 0 < log (64 / ε) := log_pos <| (one_lt_div hε₀).2 (by linarith)  obtain ⟨A₁, A₂, hA, hA₁, hA₂⟩ : ∃ (A₁ A₂ : Finset G),      1 - ε / 32 ≤ ∑ x ∈ s q' (ε / 16) univ univ A, (μ A₁ ○ᵈ μ A₂) x ∧        (4⁻¹ : ℝ) * A.dens ^ (2 * q') ≤ A₁.dens ∧ (4⁻¹ : ℝ) * A.dens ^ (2 * q') ≤ A₂.dens := by    refine sifting_cor (by positivity) (by linarith) (by positivity)      hq'even (by positivity) ?_ hA₀    calc      (ε / 16)⁻¹ * log (2 / (ε / 32)) = 2 ^ 4 * ε⁻¹ * log (64 / ε) := by ring_nf      _ ≤ q' := hq'lower  have : card G • (f ○ᵈ f) + 1 = card G • (μ A ○ᵈ μ A) := by    unfold f    rw [← balance_dddconv, balance, smul_sub, smul_const, Fintype.card_smul_expect]    simp [sum_dddconv, hA₀]  have := calc    1 + ε / 4 = 1 + ε / 2 / 2 := by ring    _ ≤ ‖card G • (f ○ᵈ f) + 1‖_[p', μ univ] := unbalancing    _ = card G • ‖(μ_[ℝ] A ○ᵈ μ A)‖_[p', μ univ] := by simp [this, wLpNorm_nsmul, -nsmul_eq_mul]    _ ≤ card G • ‖(μ_[ℝ] A ○ᵈ μ A)‖_[q', μ univ] := by      have : Nonempty G := hA₀.to_type      gcongr      exact mod_cast sum_mu ℝ≥0 univ_nonempty  let s' : Finset G := {x | 1 + ε / 8 ≤ card G • (μ A ○ᵈ μ A) x}  have hss' : s q' (ε / 16) univ univ A ⊆ s' := by    simp only [subset_iff, mem_s', ENNReal.coe_natCast, mu_univ_dddconv_mu_univ,      mem_filter, mem_univ, true_and, s']    rintro x hx    calc      1 + ε / 8 ≤ (1 - ε / 16) * (1 + ε / 4) := one_add_le_one_sub_mul_one_add <| calc          ε / 8 + ε / 16 + ε / 16 * (ε / 4) ≤ ε / 8 + ε / 16 + ε / 16 * (1 / 4) := by gcongr          _ ≤ ε / 4 := by linarith      _ ≤ (1 - ε / 16) * card G • ‖μ_[ℝ] A ○ᵈ μ A‖_[q', μ univ] := by gcongr; linarith      _ = card G • ((1 - ε / 16) * ‖μ_[ℝ] A ○ᵈ μ A‖_[q', μ univ]) := mul_smul_comm ..      _ ≤ card G • (μ A ○ᵈ μ A) x := by gcongr  obtain ⟨V, _, hVdim, hV⟩ : ∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)),    ↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤        2 ^ 32 * 𝓛 (4⁻¹ * α ^ (2 * q')) ^ 2 * 𝓛 (ε / 32 * (4⁻¹ * α ^ (2 * q'))) ^ 2 * (ε / 32)⁻¹ ^ 2          ∧ |∑ x ∈ s', (μ (Set.toFinset V) ∗ᵈ μ A₁ ○ᵈ μ A₂) x -            ∑ x ∈ s', (μ A₁ ○ᵈ μ A₂) x| ≤ ε / 32 :=    ap_in_ff' _ hq (by positivity)    (calc      4⁻¹ * (A.dens : ℝ) ^ (2 * q') ≤ 4⁻¹ * 1 := by        gcongr; exact pow_le_one₀ (by positivity) <| mod_cast A.dens_le_one      _ ≤ 2⁻¹ := by norm_num) (by positivity) (by linarith) hA₁ hA₂  replace hV :=    calc      1 - ε / 16 = 1 - ε / 32 - ε / 32 := by ring      _ ≤ ∑ x ∈ s q' (ε / 16) univ univ A, (μ A₁ ○ᵈ μ A₂) x -        |∑ x ∈ s', (μ (Set.toFinset V) ∗ᵈ μ A₁ ○ᵈ μ A₂) x - ∑ x ∈ s', (μ A₁ ○ᵈ μ A₂) x| := by gcongr      _ ≤ ∑ x ∈ s', (μ A₁ ○ᵈ μ A₂) x -        -(∑ x ∈ s', (μ (Set.toFinset V) ∗ᵈ μ A₁ ○ᵈ μ A₂) x - ∑ x ∈ s', (μ A₁ ○ᵈ μ A₂) x) := by        gcongr        · have : 0 ≤ μ_[ℝ] A₁ ○ᵈ μ A₂ := dddconv_nonneg mu_nonneg mu_nonneg          exact fun _ _ _ ↦ this _        · exact neg_le_abs _      _ = ∑ x ∈ s', (μ (Set.toFinset V) ∗ᵈ μ A₁ ○ᵈ μ A₂) x := by ring  refine ⟨V, inferInstance, ?_, ?_⟩  · calc      ↑(finrank (ZMod q) G - finrank (ZMod q) V)        ≤ 2 ^ 32 * 𝓛 (4⁻¹ * α ^ (2 * q')) ^ 2 *          𝓛 (ε / 32 * (4⁻¹ * α ^ (2 * q'))) ^ 2 * (ε / 32)⁻¹ ^ 2 := hVdim      _ ≤ 2 ^ 32 * (8 * q' * 𝓛 α) ^ 2 *          (2 ^ 8 * q' * 𝓛 α / ε) ^ 2 * (ε / 32)⁻¹ ^ 2 := by        have : α ^ (2 * q') ≤ 1 := by bound        have : 4⁻¹ * α ^ (2 * q') ≤ 1 := by bound        have : ε / 32 * (4⁻¹ * α ^ (2 * q')) ≤ 1 := by bound        have : 0 ≤ log (ε / 32 * (4⁻¹ * α ^ (2 * q')))⁻¹ := by bound        have : 0 ≤ log (4⁻¹ * α ^ (2 * q'))⁻¹ := by bound        have : 0 ≤ log (α ^ (2 * q'))⁻¹ := by bound        have := calc          𝓛 (4⁻¹ * α ^ (2 * q')) ≤ 4⁻¹⁻¹ * 𝓛 (α ^ (2 * q')) :=            curlog_mul_le (by norm_num) (by norm_num) (by positivity) ‹_›          _ ≤ 4⁻¹⁻¹ * (↑(2 * q') *  𝓛 α) := by gcongr; exact curlog_pow_le hα₀ (by positivity)          _ = 8 * q' * 𝓛 α := by push_cast; ring        gcongr        calc          𝓛 (ε / 32 * (4⁻¹ * α ^ (2 * q'))) ≤ (ε / 32)⁻¹ * 𝓛 (4⁻¹ * (α ^ (2 * q'))) :=            curlog_mul_le (by positivity) (by linarith) (by positivity) ‹_›          _ ≤ (ε / 32)⁻¹ * (8 * q' * 𝓛 α) := by gcongr          _ = 2 ^ 8 * q' * 𝓛 α / ε := by ring      _ = 2 ^ 64 * q' ^ 4 * 𝓛 α ^ 4 / ε ^ 4 := by ring      _ ≤ 2 ^ 64 * (2 ^ 16 * 𝓛 γ / ε ^ 2) ^ 4 * 𝓛 α ^ 4 / ε ^ 4 := by gcongr      _ = 2 ^ 128 * 𝓛 α ^ 4 * 𝓛 γ ^ 4 / ε ^ 12 := by ring  · rw [← le_div_iff₀ (by positivity)]    have : 0 ≤ μ_[ℝ] (Set.toFinset V) ∗ᵈ μ A₁ ○ᵈ μ A₂ :=      dddconv_nonneg (ddconv_nonneg mu_nonneg mu_nonneg) mu_nonneg    calc      1 + ε / 32 ≤ (1 + ε / 8) * (1 - ε / 16) := one_add_le_one_add_mul_one_sub <|        calc          ε / 32 + ε / 16 + ε / 8 * (ε / 16) ≤ ε / 32 + ε / 16 + ε / 8 * (1 / 16) := by gcongr          _ ≤ ε / 8 := by linarith      _ ≤ (1 + ε / 8) * ∑ x ∈ s', (μ (Set.toFinset V) ∗ᵈ μ A₁ ○ᵈ μ A₂) x := by gcongr      _ = ∑ x ∈ s', (1 + ε / 8) * (μ (Set.toFinset V) ∗ᵈ μ A₁ ○ᵈ μ A₂) x := mul_sum ..      _ ≤ ∑ x ∈ s', card G • (μ A ○ᵈ μ A) x * (μ (Set.toFinset V) ∗ᵈ μ A₁ ○ᵈ μ A₂) x := by        gcongr with x hx        · exact this _        · exact (mem_filter.1 hx).2      _ ≤ ∑ x, card G • (μ A ○ᵈ μ A) x * (μ (Set.toFinset V) ∗ᵈ μ A₁ ○ᵈ μ A₂) x := by        gcongr        · rintro x - -          have : (0 : ℝ) ≤ _ := this x          have : 0 ≤ μ_[ℝ] A ○ᵈ μ A := dddconv_nonneg mu_nonneg mu_nonneg          have : (0 : ℝ) ≤ _ := this x          positivity        · exact subset_univ _      _ = card G • ⟪μ_[ℝ] (Set.toFinset V) ∗ᵈ μ A, μ A ∗ᵈ μ A₂ ○ᵈ μ A₁⟫_[ℝ] := by        rw [← wInner_one_dddconv_eq_ddconv_wInner_one, dddconv_right_comm,          ddconv_dddconv_right_comm (μ A), wInner_one_dddconv_eq_ddconv_wInner_one,          ← dddconv_wInner_one_eq_wInner_one_ddconv, ← conj_wInner_symm]        simp only [nsmul_eq_mul, mul_assoc, wInner_one_eq_sum, inner_apply, conj_trivial, map_sum,          smul_sum]      _ ≤ card G • (‖μ_[ℝ] (Set.toFinset V) ∗ᵈ μ A‖_[∞] * ‖μ_[ℝ] A ∗ᵈ μ A₂ ○ᵈ μ A₁‖_[1]) := by        gcongr; exact wInner_one_le_dLpNorm_mul_dLpNorm _ _      _ = _ := by        have : 0 < (4 : ℝ)⁻¹ * A.dens ^ (2 * q') := by positivity        replace hA₁ : A₁.Nonempty := by simpa using this.trans_le hA₁        replace hA₂ : A₂.Nonempty := by simpa using this.trans_le hA₂        rw [dL1Norm_dddconv, dL1Norm_ddconv]        · simp [eq_div_iff, hA₀.dens_ne_zero, hA₀, hA₁, hA₂, ← card_smul_mu, smul_ddconv,            dLpNorm_nsmul, -nsmul_eq_mul]          simp [← mul_assoc, mul_comm, ddconv_comm]        · exact mu_nonneg        · exact mu_nonneg        · exact ddconv_nonneg mu_nonneg mu_nonneg        · exact mu_nonneg