Ff theorem

public theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFree (α := G) A) :    finrank (ZMod q) G ≤ 2 ^ 148 * 𝓛 A.dens ^ 9 := by  let n : ℝ := finrank (ZMod q) G  let α : ℝ := A.dens  have : 1 < (q : ℝ) := mod_cast hq₃.trans_lt' (by norm_num)  have : 1 ≤ (q : ℝ) := this.le  have : NeZero q := ⟨by positivity⟩  have : Fact q.Prime := ⟨hq⟩  have hq' : Odd q := hq.odd_of_ne_two <| by rintro rfl; simp at hq₃  have : 1 ≤ α⁻¹ := (one_le_inv₀ (by positivity)).2 (by simp [α])  have hα₀ : 0 < α := by positivity  have : 0 ≤ log α⁻¹ := log_nonneg ‹_›  have : 0 < 𝓛 α := by positivity  have : 0 < log q := log_pos ‹_›  obtain hα | hα := le_total (q ^ (n / 2) : ℝ) (2 * α⁻¹ ^ 2)  · rw [rpow_le_iff_le_log, log_mul, log_pow, Nat.cast_two, ← mul_div_right_comm,      mul_div_assoc, ← le_div_iff₀] at hα    any_goals positivity    calc      _ ≤ (log 2 + 2 * log α⁻¹) / (log q / 2) := hα      _ = 4 / log q * (log 2 / 2 + log α⁻¹) := by ring      _ ≤ 2 ^ 148 * 𝓛 α ^ 9 := by        grw [← hq₃, pow_succ _ 8, ← mul_assoc, log_two_lt_d9]        gcongr        · norm_cast          grw [← log_three_gt_d9, ← ‹1 ≤ α⁻¹›]          norm_num        · bound  have ind (i : ℕ) :    ∃ (V : Type u) (_ : AddCommGroup V) (_ : Fintype V) (_ : DecidableEq V) (_ : Module (ZMod q) V)      (B : Finset V), n ≤ finrank (ZMod q) V + 2 ^ 140 * i * 𝓛 α ^ 8 ∧ ThreeAPFree (B : Set V)        ∧ α ≤ B.dens ∧      (B.dens < (65 / 64 : ℝ) ^ i * α →        2⁻¹ ≤ card V * ⟪μ_[ℝ] B ∗ᵈ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by    induction i with    | zero =>      classical      exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp [n], hA,        by simp [α], by simp [α, nnratCast_dens]⟩    | succ i ih =>    obtain ⟨V, _, _, _, _, B, hV, hB, hαβ, hBV⟩ := ih    obtain hB' | hB' := le_or_gt 2⁻¹ (card V * ⟪μ_[ℝ] B ∗ᵈ μ B, μ (B.image (2 • ·))⟫_[ℝ])    · exact ⟨V, inferInstance, inferInstance, inferInstance, inferInstance, B,        hV.trans (by gcongr; exact i.le_succ), hB, hαβ, fun _ ↦ hB'⟩    let : MeasurableSpace V := ⊤    have : 0 < 𝓛 B.dens := curlog_pos (by positivity) (by simp)    have : 2⁻¹ ≤ |card V * ⟪μ_[ℝ] B ∗ᵈ μ B, μ (B.image (2 • ·))⟫_[ℝ] - 1| := by      rw [abs_sub_comm, le_abs, le_sub_comm]      norm_num at hB' ⊢      exact .inl hB'.le    obtain ⟨V', _, hVV', hv'⟩ := di_in_ff hq (by positivity) two_inv_lt_one (by      rwa [Finset.dens_image (Nat.Coprime.nsmul_right_bijective _)]      simpa [Module.card_eq_pow_finrank (K := ZMod q) (V := V), ZMod.card] using hq'.pow) hα₀ this    rw [dLinftyNorm_eq_iSup_norm, ← Finset.sup'_univ_eq_ciSup, Finset.le_sup'_iff] at hv'    obtain ⟨x, -, hx⟩ := hv'    let B' : Finset V' := (-x +ᵥ B).preimage (↑) Set.injOn_subtype_val    have hβ := calc      ((1 + 64⁻¹ : ℝ) * B.dens : ℝ) = (1 + 2⁻¹ / 32) * B.dens := by ring      _ ≤ ‖(𝟭_[(B : Set V), ℝ] ∗ᵈ μ (V' : Set V).toFinset) x‖ := hx      _ = B'.dens := by        rw [Real.norm_of_nonneg (ddconv_apply_nonneg Set.indicator_one_nonneg mu_nonneg _),          dens_addSubgroup_preimage_vadd_eq_indicator_one_ddconv_mu]    refine ⟨V', inferInstance, inferInstance, inferInstance, inferInstance, B', ?_, ?_, ?_,      fun h ↦ ?_⟩    · calc        n ≤ finrank (ZMod q) V + 2 ^ 140 * i * 𝓛 α ^ 8 := hV        _ ≤ finrank (ZMod q) V' + ↑(finrank (ZMod q) V - finrank (ZMod q) V') +            2 ^ 140 * i * 𝓛 α ^ 8 := by gcongr; norm_cast; exact le_add_tsub        _ ≤ finrank (ZMod q) V' + 2 ^ 128 * 𝓛 B.dens ^ 4 * 𝓛 α ^ 4 / 2⁻¹ ^ 12 +            2 ^ 140 * i * 𝓛 α ^ 8 := by gcongr        _ ≤ finrank (ZMod q) V' + 2 ^ 128 * 𝓛 α ^ 4 * 𝓛 α ^ 4 / 2⁻¹ ^ 12 +            2 ^ 140 * i * 𝓛 α ^ 8 := by have := hα₀.trans_le hαβ; gcongr        _ = _ := by push_cast; ring    · exact .of_image .subtypeVal Set.injOn_subtype_val (Set.subset_univ _)        (hB.vadd_set (a := -x) |>.mono <| by simp [B'])    · calc        α ≤ B.dens := hαβ        _ ≤ (1 + 64⁻¹) * B.dens := by simp [one_add_mul, NNRat.cast_nonneg]        _ ≤ B'.dens := hβ    · refine (h.not_ge <| ?_).elim      calc        (65 / 64) ^ (i + 1) * α = (1 + 64⁻¹) * ((65 / 64) ^ i * α) := by ring        _ ≤ (1 + 64⁻¹) * B.dens := by gcongr; simpa [hB'.not_ge] using hBV        _ ≤ B'.dens := hβ  obtain ⟨V, _, _, _, _, B, hV, hB, hαβ, hBV⟩ := ind ⌊𝓛 α / log (65 / 64)⌋₊  let β : ℝ := B.dens  have aux : 0 < log (65 / 64) := log_pos (by norm_num)  specialize hBV <| by    calc      _ ≤ (1 : ℝ) := mod_cast dens_le_one      _ < _ := ?_    rw [← inv_lt_iff_one_lt_mul₀, lt_pow_iff_log_lt, ← div_lt_iff₀]    any_goals positivity    calc      log α⁻¹ / log (65 / 64)        < ⌊log α⁻¹ / log (65 / 64)⌋₊ + 1 := Nat.lt_floor_add_one _      _ = ⌊(log (65 / 64) + log α⁻¹) / log (65 / 64)⌋₊ := by        rw [add_comm (log _), ← div_add_one aux.ne', Nat.floor_add_one, Nat.cast_succ]        bound      _ ≤ ⌊𝓛 α / log (65 / 64)⌋₊ := by        gcongr        calc          log (65 / 64) ≤ 65/64 - 1 := log_le_sub_one_of_pos <| by norm_num          _ ≤ 1 := by norm_num  rw [hB.wInner_one_mu_ddconv_mu_mu_two_smul_mu] at hBV  swap  · simpa [Module.card_eq_pow_finrank (K := ZMod q) (V := V), ZMod.card] using hq'.pow  suffices h : (q ^ (n - 2 ^ 147 * 𝓛 α ^ 9) : ℝ) ≤ q ^ (n / 2) by    rwa [rpow_le_rpow_left_iff ‹_›, sub_le_comm, sub_half, div_le_iff₀' zero_lt_two, ← mul_assoc,      ← pow_succ'] at h  calc    _ ≤ ↑q ^ (finrank (ZMod q) V : ℝ) := by      gcongr      rw [sub_le_comm]      calc        n - finrank (ZMod q) V ≤ 2 ^ 140 * ⌊𝓛 α / log (65 / 64)⌋₊ * 𝓛 α ^ 8 := by          rwa [sub_le_iff_le_add']        _ ≤ 2 ^ 140 * (𝓛 α / log (65 / 64)) * 𝓛 α ^ 8 := by          gcongr; exact Nat.floor_le (by positivity)        _ = 2 ^ 140 * (log (65 / 64)) ⁻¹ * 𝓛 α ^ 9 := by ring        _ ≤ 2 ^ 140 * 2 ^ 7 * 𝓛 α ^ 9 := by          gcongr          refine inv_le_of_inv_le₀ (by positivity) ?_          calc            (2 ^ 7)⁻¹ ≤ 1 - (65 / 64)⁻¹ := by norm_num            _ ≤ log (65 / 64) := one_sub_inv_le_log_of_pos (by positivity)        _ = 2 ^ 147 * 𝓛 α ^ 9 := by ring    _ = ↑(card V) := by simp [Module.card_eq_pow_finrank (K := ZMod q) (V := V)]    _ ≤ 2 * β⁻¹ ^ 2 := by      rw [← natCast_card_mul_nnratCast_dens, mul_pow, mul_inv, ← mul_assoc,        ← div_eq_mul_inv (card V : ℝ), ← zpow_one_sub_natCast₀ (by positivity)] at hBV      have : 0 < (card V : ℝ) := by positivity      simpa [le_inv_mul_iff₀, mul_inv_le_iff₀, this, zero_lt_two, mul_comm] using hBV    _ ≤ 2 * α⁻¹ ^ 2 := by gcongr    _ ≤ _ := hα