Erdős problem 18 - b

open Finset Filter

theorem exact_target_type :
    (fcTypeOfName% "Erdos18.erdos_18b") =
      (True ↔ ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in Filter.atTop,
        (Erdos18.practicalH n.factorial : ℝ) < (n : ℝ) ^ ε) := by
  rfl

def HasShortDivisorSum (N R k : ℕ) : Prop :=
  ∃ D : Finset ℕ, D ⊆ N.divisors ∧ D.sum id = R ∧ D.card ≤ k

theorem short_sum_zero (N k : ℕ) : HasShortDivisorSum N 0 k := by
  refine ⟨∅, ?_, ?_, ?_⟩ <;> simp

theorem short_sum_mono_count {N R k l : ℕ}
    (h : HasShortDivisorSum N R k) (hkl : k ≤ l) :
    HasShortDivisorSum N R l := by
  obtain ⟨D, hD, hsum, hcard⟩ := h
  exact ⟨D, hD, hsum, hcard.trans hkl⟩

theorem short_sum_mono_host {N M R k : ℕ}
    (hNM : N ∣ M) (hM : M ≠ 0) (h : HasShortDivisorSum N R k) :
    HasShortDivisorSum M R k := by
  obtain ⟨D, hD, hsum, hcard⟩ := h
  exact ⟨D, hD.trans (Nat.divisors_subset_of_dvd hM hNM), hsum, hcard⟩

theorem practicalH_le_of_short_sums (N k : ℕ)
    (h : ∀ R ∈ Finset.Icc 1 N, HasShortDivisorSum N R k) :
    Erdos18.practicalH N ≤ k := by
  classical
  unfold Erdos18.practicalH
  apply Finset.sup_le
  intro R hR
  obtain ⟨D, hD, hsum, hcard⟩ := h R hR
  apply le_trans ?_ hcard
  apply Nat.sInf_le
  exact ⟨D, hD, rfl, D, Set.Subset.rfl, hsum.symm⟩

theorem short_sum_of_practicalH {N R : ℕ}
    (hN : Nat.IsPractical N) (hR : R ≤ N) :
    HasShortDivisorSum N R (Erdos18.practicalH N) := by
  classical
  by_cases hzero : R = 0
  · subst R
    exact short_sum_zero _ _
  have hRmem : R ∈ Finset.Icc 1 N := Finset.mem_Icc.mpr ⟨by omega, hR⟩
  have hne : {k | ∃ D : Finset ℕ,
      D ⊆ N.divisors ∧ D.card = k ∧ R ∈ subsetSums D}.Nonempty :=
    ⟨N.divisors.card, N.divisors, Finset.Subset.refl _, rfl, hN R hR⟩
  obtain ⟨D, hD, hcard, E, hED, hsum⟩ := Nat.sInf_mem hne
  have hsub : E ⊆ D := Finset.coe_subset.mp hED
  refine ⟨E, hsub.trans hD, hsum.symm, ?_⟩
  calc
    E.card ≤ D.card := Finset.card_le_card hsub
    _ = sInf {k | ∃ D : Finset ℕ,
        D ⊆ N.divisors ∧ D.card = k ∧ R ∈ subsetSums D} := hcard
    _ ≤ Erdos18.practicalH N := by
      exact Finset.le_sup (f := fun m => sInf {k | ∃ D : Finset ℕ,
        D ⊆ N.divisors ∧ D.card = k ∧ m ∈ subsetSums D}) hRmem

theorem short_sum_radix {M q a r k l : ℕ}
    (hM : 0 < M) (hq : 0 < q) (hrq : r < q)
    (ha : HasShortDivisorSum M a k)
    (hr : HasShortDivisorSum (q * M) r l) :
    HasShortDivisorSum (q * M) (q * a + r) (k + l) := by
  classical
  obtain ⟨A, hA, hAsum, hAcard⟩ := ha
  obtain ⟨B, hB, hBsum, hBcard⟩ := hr
  have hinj : Function.Injective (fun d : ℕ => q * d) :=
    fun _ _ h => mul_left_cancel₀ (ne_of_gt hq) h
  have hdisj : Disjoint (A.image (fun d => q * d)) B := by
    apply Finset.disjoint_left.mpr
    intro x hx hxB
    obtain ⟨d, hd, rfl⟩ := Finset.mem_image.mp hx
    have hdpos : 0 < d := Nat.pos_of_dvd_of_pos
      (Nat.dvd_of_mem_divisors (hA hd)) hM
    have hlow : q ≤ q * d := by nlinarith
    have hhigh : q * d ≤ r := by
      rw [← hBsum]
      exact Finset.single_le_sum (f := id) (fun _ _ => Nat.zero_le _) hxB
    omega
  refine ⟨A.image (fun d => q * d) ∪ B, ?_, ?_, ?_⟩
  · intro x hx
    rcases Finset.mem_union.mp hx with hx | hx
    · obtain ⟨d, hd, rfl⟩ := Finset.mem_image.mp hx
      exact Nat.mem_divisors.mpr
        ⟨mul_dvd_mul_left q (Nat.dvd_of_mem_divisors (hA hd)),
          ne_of_gt (Nat.mul_pos hq hM)⟩
    · exact hB hx
  · rw [Finset.sum_union hdisj, Finset.sum_image
      (fun x _ y _ h => hinj h)]
    change (∑ x ∈ A, q * x) + B.sum id = q * a + r
    rw [← Finset.mul_sum, show (∑ x ∈ A, x) = a from hAsum, hBsum]
  · rw [Finset.card_union_of_disjoint hdisj,
      Finset.card_image_of_injective A hinj]
    omega

theorem practicalH_radix {M q l : ℕ}
    (hM : Nat.IsPractical M) (hMpos : 0 < M) (hq : 0 < q)
    (hlocal : ∀ r < q, HasShortDivisorSum (q * M) r l) :
    Erdos18.practicalH (q * M) ≤ Erdos18.practicalH M + l := by
  apply practicalH_le_of_short_sums
  intro R hR
  have hquot : R / q ≤ M :=
    Nat.div_le_of_le_mul (Finset.mem_Icc.mp hR).2
  have hrep := short_sum_radix hMpos hq (Nat.mod_lt R hq)
    (short_sum_of_practicalH hM hquot) (hlocal (R % q) (Nat.mod_lt R hq))
  simpa only [Nat.div_add_mod] using hrep

theorem factorial_radix_recurrence {n m l : ℕ} (hmn : m ≤ n)
    (hlocal : ∀ r < n.factorial / m.factorial,
      HasShortDivisorSum n.factorial r l) :
    Erdos18.practicalH n.factorial ≤ Erdos18.practicalH m.factorial + l := by
  have hdiv : m.factorial ∣ n.factorial := Nat.factorial_dvd_factorial hmn
  have heq : n.factorial / m.factorial * m.factorial = n.factorial :=
    Nat.div_mul_cancel hdiv
  have hq : 0 < n.factorial / m.factorial :=
    Nat.div_pos (Nat.le_of_dvd (Nat.factorial_pos n) hdiv) (Nat.factorial_pos m)
  have h := practicalH_radix (Erdos18.factorial_isPractical m)
    (Nat.factorial_pos m) hq (by simpa only [heq] using hlocal)
  simpa only [heq] using h

theorem positive_quotient_of_dvd {R S q : ℕ}
    (hq : 0 < q) (hSR : S < R) (hdvd : q ∣ R - S) :
    ∃ t : ℕ, 0 < t ∧ R = S + q * t ∧ t ≤ R / q := by
  refine ⟨(R - S) / q, ?_, ?_, ?_⟩
  · exact Nat.div_pos (Nat.le_of_dvd (Nat.sub_pos_of_lt hSR) hdvd) hq
  · rw [Nat.mul_div_cancel' hdvd]
    exact (Nat.add_sub_of_le hSR.le).symm
  · exact Nat.div_le_div_right (Nat.sub_le R S)

theorem polynomial_height_below_target {R S q D : ℕ}
    (hq : 2 ≤ q) (hR : q ^ (D + 1) ≤ R) (hS : S ≤ q ^ D) :
    S < R ∧ 2 * S ≤ R := by
  have hpow : 0 < q ^ D := pow_pos (by omega) D
  rw [pow_succ] at hR
  constructor <;> nlinarith

theorem positive_lifting_of_polynomial_height {R S q D : ℕ}
    (hq : 2 ≤ q) (hR : q ^ (D + 1) ≤ R) (hS : S ≤ q ^ D)
    (hdvd : q ∣ R - S) :
    ∃ t : ℕ, 0 < t ∧ R = S + q * t ∧ t ≤ R / q := by
  exact positive_quotient_of_dvd (by omega)
    (polynomial_height_below_target hq hR hS).1 hdvd

theorem positive_lifting_of_congruence {R S q D : ℕ}
    (hq : 2 ≤ q) (hR : q ^ (D + 1) ≤ R) (hS : S ≤ q ^ D)
    (hmod : Nat.ModEq q S R) :
    ∃ t : ℕ, 0 < t ∧ R = S + q * t ∧ t ≤ R / q := by
  exact positive_lifting_of_polynomial_height hq hR hS hmod.dvd'

theorem factorial_power_dvd (m r : ℕ) :
    m.factorial ^ r ∣ (r * m).factorial := by
  simpa using Nat.prod_factorial_dvd_factorial_sum (Finset.range r) (fun _ => m)

theorem factorial_binary_reserve (m k : ℕ) :
    2 ^ k * m.factorial ∣ (m + 2 * k).factorial := by
  have hpow : 2 ^ k ∣ (2 * k).factorial := by
    simpa [Nat.factorial, Nat.mul_comm] using factorial_power_dvd 2 k
  exact (mul_dvd_mul hpow (dvd_refl m.factorial)).trans
    (by simpa [Nat.add_comm] using
      Nat.factorial_mul_factorial_dvd_factorial_add (2 * k) m)

theorem shifted_divisor_dvd_factorial {m k b d : ℕ}
    (hd : d ∣ m.factorial) (hb : b ≤ k) :
    2 ^ b * d ∣ (m + 2 * k).factorial := by
  exact (mul_dvd_mul (pow_dvd_pow 2 hb) hd).trans (factorial_binary_reserve m k)

theorem product_divisors_dvd_factorial_sum {ι : Type*}
    (I : Finset ι) (d a : ι → ℕ)
    (h : ∀ i ∈ I, d i ∣ (a i).factorial) :
    (∏ i ∈ I, d i) ∣ (∑ i ∈ I, a i).factorial := by
  exact (Finset.prod_dvd_prod_of_dvd d (fun i => (a i).factorial) h).trans
    (Nat.prod_factorial_dvd_factorial_sum I a)

theorem distinctify_divisor_multiset (s : Multiset ℕ) {N : ℕ}
    (hN : N ≠ 0) (hs : ∀ d ∈ s, d ∣ N) :
    HasShortDivisorSum (2 ^ s.card * N) s.sum s.card := by
  classical
  have aux : ∀ k : ℕ, ∀ t : Multiset ℕ, t.card = k →
      ∀ M : ℕ, M ≠ 0 → (∀ d ∈ t, d ∣ M) →
      HasShortDivisorSum (2 ^ k * M) t.sum k := by
    intro k
    induction k using Nat.strong_induction_on with
    | h k ih =>
      intro t hk M hM ht
      by_cases hn : t.Nodup
      · refine ⟨t.toFinset, ?_, ?_, ?_⟩
        · intro d hd
          exact Nat.mem_divisors.mpr
            ⟨dvd_mul_of_dvd_right (ht d (Multiset.mem_toFinset.mp hd)) (2 ^ k),
              mul_ne_zero (pow_ne_zero _ (by decide)) hM⟩
        · change (t.toFinset.val.map id).sum = t.sum
          simp [hn.dedup]
        · exact le_of_eq ((Multiset.toFinset_card_of_nodup hn).trans hk)
      · rw [Multiset.nodup_iff_ne_cons_cons] at hn
        push Not at hn
        obtain ⟨a, u, rfl⟩ := hn
        have hc : (2 * a ::ₘ u).card < k := by
          simp only [Multiset.card_cons] at hk ⊢
          omega
        have hnew : ∀ d ∈ (2 * a ::ₘ u), d ∣ 2 * M := by
          intro d hd
          rcases Multiset.mem_cons.mp hd with rfl | hd
          · exact mul_dvd_mul_left 2 (ht a (by simp))
          · exact dvd_mul_of_dvd_right (ht d (by simp [hd])) 2
        have hrep := ih _ hc (2 * a ::ₘ u) rfl (2 * M)
          (mul_ne_zero (by decide) hM) hnew
        have hhost : 2 ^ (2 * a ::ₘ u).card * (2 * M) = 2 ^ k * M := by
          rw [← hk]
          simp only [Multiset.card_cons, pow_succ]
          ring
        have hsum : (2 * a ::ₘ u).sum = (a ::ₘ a ::ₘ u).sum := by
          simp [two_mul, add_assoc]
        have hrep' := short_sum_mono_count hrep hc.le
        simpa only [hhost, hsum] using hrep'
  exact aux s.card s rfl N hN hs

theorem distinctify_factorial_divisors (s : Multiset ℕ) (F : ℕ)
    (hs : ∀ d ∈ s, d ∣ F.factorial) :
    HasShortDivisorSum (F + 2 * s.card).factorial s.sum s.card := by
  exact short_sum_mono_host (factorial_binary_reserve F s.card)
    (Nat.factorial_ne_zero _) (distinctify_divisor_multiset s (Nat.factorial_ne_zero F) hs)

def HasFactorialDivisorMultiset (F R u : ℕ) : Prop :=
  ∃ s : Multiset ℕ, (∀ d ∈ s, d ∣ F.factorial) ∧ s.sum = R ∧ s.card ≤ u

theorem factorial_multiset_zero (F u : ℕ) : HasFactorialDivisorMultiset F 0 u := by
  exact ⟨0, by simp, by simp, by simp⟩

theorem factorial_multiset_singleton {F R : ℕ} (hR : R ∣ F.factorial) :
    HasFactorialDivisorMultiset F R 1 := by
  exact ⟨{R}, by simpa using hR, by simp, by simp⟩

theorem factorial_multiset_mono {F G R u v : ℕ}
    (h : HasFactorialDivisorMultiset F R u) (hFG : F ≤ G) (huv : u ≤ v) :
    HasFactorialDivisorMultiset G R v := by
  obtain ⟨s, hs, hsum, hcard⟩ := h
  exact ⟨s, fun d hd => (hs d hd).trans (Nat.factorial_dvd_factorial hFG),
    hsum, hcard.trans huv⟩

theorem factorial_multiset_to_distinct {F R u : ℕ}
    (h : HasFactorialDivisorMultiset F R u) :
    HasShortDivisorSum (F + 2 * u).factorial R u := by
  obtain ⟨s, hs, hsum, hcard⟩ := h
  have hrep := distinctify_factorial_divisors s F hs
  rw [hsum] at hrep
  exact short_sum_mono_count
    (short_sum_mono_host (Nat.factorial_dvd_factorial (by omega))
      (Nat.factorial_ne_zero (F + 2 * u)) hrep) hcard

theorem factorial_multiset_add {F R S u v : ℕ}
    (hR : HasFactorialDivisorMultiset F R u)
    (hS : HasFactorialDivisorMultiset F S v) :
    HasFactorialDivisorMultiset F (R + S) (u + v) := by
  obtain ⟨s, hs, hsum, hcard⟩ := hR
  obtain ⟨t, ht, htsum, htcard⟩ := hS
  refine ⟨s + t, ?_, ?_, ?_⟩
  · intro d hd
    rcases Multiset.mem_add.mp hd with hd | hd
    · exact hs d hd
    · exact ht d hd
  · simp only [Multiset.sum_add, hsum, htsum]
  · simpa only [Multiset.card_add] using Nat.add_le_add hcard htcard

theorem factorial_multiset_scale {F G q R u : ℕ}
    (hq : q ∣ F.factorial) (h : HasFactorialDivisorMultiset G R u) :
    HasFactorialDivisorMultiset (F + G) (q * R) u := by
  obtain ⟨s, hs, hsum, hcard⟩ := h
  refine ⟨s.map (fun d => q * d), ?_, ?_, ?_⟩
  · intro x hx
    obtain ⟨d, hd, rfl⟩ := Multiset.mem_map.mp hx
    exact (mul_dvd_mul hq (hs d hd)).trans
      (Nat.factorial_mul_factorial_dvd_factorial_add F G)
  · have hmul := Multiset.sum_map_mul_left (s := s) (a := q) (f := id)
    simpa [hsum] using hmul
  · simpa only [Multiset.card_map] using hcard

theorem multiset_sum_expansion (s t : Multiset ℕ) :
    ((s ×ˢ t).map (fun p => p.1 * p.2)).sum = s.sum * t.sum := by
  refine Multiset.induction_on s (by simp) fun a s ih => ?_
  have hmul := Multiset.sum_map_mul_left (s := t) (a := a) (f := id)
  simp only [Multiset.cons_product, Multiset.map_add, Multiset.map_map,
    Multiset.sum_add, Multiset.sum_cons, ih]
  simpa [Function.comp_def, add_mul] using congrArg (fun x => x + s.sum * t.sum) hmul

theorem factorial_multiset_mul {F G R S u v : ℕ}
    (hR : HasFactorialDivisorMultiset F R u)
    (hS : HasFactorialDivisorMultiset G S v) :
    HasFactorialDivisorMultiset (F + G) (R * S) (u * v) := by
  obtain ⟨s, hs, hsum, hcard⟩ := hR
  obtain ⟨t, ht, htsum, htcard⟩ := hS
  refine ⟨(s ×ˢ t).map (fun p => p.1 * p.2), ?_, ?_, ?_⟩
  · intro d hd
    obtain ⟨⟨a, b⟩, hab, rfl⟩ := Multiset.mem_map.mp hd
    obtain ⟨ha, hb⟩ := Multiset.mem_product.mp hab
    exact (mul_dvd_mul (hs a ha) (ht b hb)).trans
      (Nat.factorial_mul_factorial_dvd_factorial_add F G)
  · simp only [multiset_sum_expansion, hsum, htsum]
  · simpa only [Multiset.card_map, Multiset.card_product] using
      Nat.mul_le_mul hcard htcard

theorem factorial_multiset_lift {F G q R S T u v : ℕ}
    (hq : q ∣ F.factorial) (hR : R = S + q * T)
    (hS : HasFactorialDivisorMultiset F S u)
    (hT : HasFactorialDivisorMultiset G T v) :
    HasFactorialDivisorMultiset (F + G) R (u + v) := by
  rw [hR]
  exact factorial_multiset_add (factorial_multiset_mono hS (by omega) le_rfl)
    (factorial_multiset_scale hq hT)

def HasBoundedModularRepresentatives (q F u D : ℕ) : Prop :=
  ∀ R : ℕ, ∃ S : ℕ, S ≤ q ^ D ∧ Nat.ModEq q S R ∧
    HasFactorialDivisorMultiset F S u

theorem positive_modular_lifting_step {q F G u v D R : ℕ}
    (hq : 2 ≤ q) (hdiv : q ∣ F.factorial) (hR : q ^ (D + 1) ≤ R)
    (hmod : HasBoundedModularRepresentatives q F u D)
    (hchild : ∀ T : ℕ, 0 < T → T ≤ R / q → HasFactorialDivisorMultiset G T v) :
    HasFactorialDivisorMultiset (F + G) R (u + v) := by
  obtain ⟨S, hS, hcongr, hrep⟩ := hmod R
  obtain ⟨T, hTpos, hidentity, hTbound⟩ :=
    positive_lifting_of_congruence hq hR hS hcongr
  exact factorial_multiset_lift hdiv hidentity hrep (hchild T hTpos hTbound)

theorem positive_modular_lifting_step_distinct {q F G u v D R : ℕ}
    (hq : 2 ≤ q) (hdiv : q ∣ F.factorial) (hR : q ^ (D + 1) ≤ R)
    (hmod : HasBoundedModularRepresentatives q F u D)
    (hchild : ∀ T : ℕ, 0 < T → T ≤ R / q → HasFactorialDivisorMultiset G T v) :
    HasShortDivisorSum (F + G + 2 * (u + v)).factorial R (u + v) := by
  exact factorial_multiset_to_distinct
    (positive_modular_lifting_step hq hdiv hR hmod hchild)

theorem recursive_modular_lifting
    (indexBudget countBudget : ℕ → ℕ) (threshold : ℕ)
    (hbase : ∀ R < threshold,
      HasFactorialDivisorMultiset (indexBudget R) R (countBudget R))
    (hstep : ∀ R, threshold ≤ R → ∃ q F u D : ℕ,
      2 ≤ q ∧ q ∣ F.factorial ∧ q ^ (D + 1) ≤ R ∧
      HasBoundedModularRepresentatives q F u D ∧
      ∀ T : ℕ, 0 < T → T ≤ R / q →
        F + indexBudget T ≤ indexBudget R ∧
        u + countBudget T ≤ countBudget R) :
    ∀ R : ℕ, HasFactorialDivisorMultiset (indexBudget R) R (countBudget R) := by
  intro R
  induction R using Nat.strong_induction_on with
  | h R ih =>
    by_cases hsmall : R < threshold
    · exact hbase R hsmall
    obtain ⟨q, F, u, D, hq, hdiv, hheight, hmod, hbudget⟩ :=
      hstep R (by omega)
    obtain ⟨S, hS, hcongr, hrep⟩ := hmod R
    obtain ⟨T, hTpos, hidentity, hTbound⟩ :=
      positive_lifting_of_congruence hq hheight hS hcongr
    have hRpos : 0 < R := lt_of_lt_of_le (pow_pos (by omega) _) hheight
    have hTlt : T < R := hTbound.trans_lt (Nat.div_lt_self hRpos (by omega))
    have hchild := ih T hTlt
    obtain ⟨hF, hu⟩ := hbudget T hTpos hTbound
    exact factorial_multiset_mono
      (factorial_multiset_lift hdiv hidentity hrep hchild) hF hu

theorem bounded_recursive_modular_lifting
    (φ ψ : ℕ → ℝ) (threshold : ℕ) (C E A B ρ σ : ℝ)
    (hφ : ∀ R : ℕ, 0 < R → 1 ≤ φ R)
    (hψ : ∀ R : ℕ, 0 < R → 1 ≤ ψ R)
    (hC : (threshold : ℝ) ≤ C) (hCpos : 0 ≤ C)
    (hE : 1 ≤ E)
    (hindex : A + C * ρ ≤ C) (hcount : B + E * σ ≤ E)
    (hstep : ∀ R : ℕ, 0 < R → threshold ≤ R → ∃ q F u D : ℕ,
      2 ≤ q ∧ q ∣ F.factorial ∧ q ^ (D + 1) ≤ R ∧
      HasBoundedModularRepresentatives q F u D ∧
      (F : ℝ) ≤ A * φ R ∧ (u : ℝ) ≤ B * ψ R ∧
      ∀ T : ℕ, 0 < T → T ≤ R / q →
        φ T ≤ ρ * φ R ∧ ψ T ≤ σ * ψ R) :
    ∀ R : ℕ, 0 < R → ∃ F u : ℕ,
      HasFactorialDivisorMultiset F R u ∧
      (F : ℝ) ≤ C * φ R ∧ (u : ℝ) ≤ E * ψ R := by
  have hEpos : 0 ≤ E := by linarith
  intro R
  induction R using Nat.strong_induction_on with
  | h R ih =>
    intro hRpos
    by_cases hsmall : R < threshold
    · refine ⟨R, 1, factorial_multiset_singleton (Nat.dvd_factorial hRpos le_rfl), ?_, ?_⟩
      · have hRle : (R : ℝ) ≤ threshold := by exact_mod_cast hsmall.le
        have hprod : C ≤ C * φ R := by nlinarith [hφ R hRpos]
        exact hRle.trans (hC.trans hprod)
      · have hprod : E ≤ E * ψ R := by nlinarith [hψ R hRpos]
        simpa only [Nat.cast_one] using hE.trans hprod
    obtain ⟨q, F, u, D, hq, hdiv, hheight, hmod, hF, hu, hshrink⟩ :=
      hstep R hRpos (by omega)
    obtain ⟨S, hS, hcongr, hrep⟩ := hmod R
    obtain ⟨T, hTpos, hidentity, hTbound⟩ :=
      positive_lifting_of_congruence hq hheight hS hcongr
    have hTlt : T < R := hTbound.trans_lt (Nat.div_lt_self hRpos (by omega))
    obtain ⟨G, v, hchild, hG, hv⟩ := ih T hTlt hTpos
    obtain ⟨hφT, hψT⟩ := hshrink T hTpos hTbound
    refine ⟨F + G, u + v, factorial_multiset_lift hdiv hidentity hrep hchild, ?_, ?_⟩
    · calc
        ((F + G : ℕ) : ℝ) = (F : ℝ) + G := Nat.cast_add _ _
        _ ≤ A * φ R + C * φ T := add_le_add hF hG
        _ ≤ A * φ R + C * (ρ * φ R) := by gcongr
        _ = (A + C * ρ) * φ R := by ring
        _ ≤ C * φ R := mul_le_mul_of_nonneg_right hindex (by linarith [hφ R hRpos])
    · calc
        ((u + v : ℕ) : ℝ) = (u : ℝ) + v := Nat.cast_add _ _
        _ ≤ B * ψ R + E * ψ T := add_le_add hu hv
        _ ≤ B * ψ R + E * (σ * ψ R) := by gcongr
        _ = (B + E * σ) * ψ R := by ring
        _ ≤ E * ψ R := mul_le_mul_of_nonneg_right hcount (by linarith [hψ R hRpos])

def binaryLength (R : ℕ) : ℕ := Nat.log 2 R + 1

def liftingBits (R D : ℕ) : ℕ := Nat.log 2 R / (D + 1)

theorem binaryLength_pos (R : ℕ) : 0 < binaryLength R := by
  simp [binaryLength]

theorem lifting_modulus_height {R D : ℕ} (hR : 0 < R) :
    (2 ^ liftingBits R D) ^ (D + 1) ≤ R := by
  unfold liftingBits
  rw [← pow_mul]
  exact (Nat.pow_le_pow_right (by decide : 0 < 2)
    (Nat.div_mul_le_self (Nat.log 2 R) (D + 1))).trans
    (Nat.pow_log_le_self 2 hR.ne')

theorem liftingBits_pos {R D : ℕ} (hR : D + 1 ≤ Nat.log 2 R) :
    0 < liftingBits R D := by
  exact Nat.div_pos hR (by omega)

theorem lifting_modulus_ge_two {R D : ℕ} (hR : D + 1 ≤ Nat.log 2 R) :
    2 ≤ 2 ^ liftingBits R D := by
  simpa using Nat.pow_le_pow_right (by decide : 0 < 2) (liftingBits_pos hR)

theorem liftingBits_le_binaryLength (R D : ℕ) :
    liftingBits R D ≤ binaryLength R := by
  exact (Nat.div_le_self _ _).trans (Nat.le_succ _)

noncomputable def liftingRatio (D : ℕ) : ℝ := 1 - 1 / (2 * ((D : ℝ) + 1))

theorem liftingRatio_pos (D : ℕ) : 0 < liftingRatio D := by
  have hD : (0 : ℝ) ≤ D := Nat.cast_nonneg D
  unfold liftingRatio
  have : 1 / (2 * ((D : ℝ) + 1)) < 1 :=
    (div_lt_one (by positivity)).mpr (by linarith)
  linarith

theorem liftingRatio_lt_one (D : ℕ) : liftingRatio D < 1 := by
  unfold liftingRatio
  have : 0 < 1 / (2 * ((D : ℝ) + 1)) := by positivity
  linarith

theorem binaryLength_quotient_shrink {R T D : ℕ}
    (hR : D + 1 ≤ Nat.log 2 R) (hT : T ≤ R / 2 ^ liftingBits R D) :
    (binaryLength T : ℝ) ≤ liftingRatio D * (binaryLength R : ℝ) := by
  have hkpos : 0 < liftingBits R D := liftingBits_pos hR
  have hk : liftingBits R D ≤ Nat.log 2 R := Nat.div_le_self _ _
  have hlog : Nat.log 2 T ≤ Nat.log 2 R - liftingBits R D := by
    calc
      Nat.log 2 T ≤ Nat.log 2 (R / 2 ^ liftingBits R D) := Nat.log_mono_right hT
      _ = Nat.log 2 R - liftingBits R D := Nat.log_div_base_pow 2 R _
  have hsplit : Nat.log 2 T + liftingBits R D ≤ Nat.log 2 R := by omega
  have hdiv : Nat.log 2 R < (D + 1) * (liftingBits R D + 1) :=
    Nat.lt_mul_div_succ _ (by omega)
  have hgap : binaryLength R ≤ 2 * (D + 1) * liftingBits R D := by
    unfold binaryLength
    nlinarith
  have hsplitR : (binaryLength T : ℝ) + (liftingBits R D : ℝ) ≤ binaryLength R := by
    exact_mod_cast (show binaryLength T + liftingBits R D ≤ binaryLength R by
      unfold binaryLength
      omega)
  have hgapR : (binaryLength R : ℝ) ≤
      (2 * ((D : ℝ) + 1)) * (liftingBits R D : ℝ) := by exact_mod_cast hgap
  have hden : (0 : ℝ) < 2 * ((D : ℝ) + 1) := by positivity
  have hquot : (binaryLength R : ℝ) / (2 * ((D : ℝ) + 1)) ≤ liftingBits R D :=
    (div_le_iff₀ hden).mpr (by nlinarith [hgapR])
  unfold liftingRatio
  have hid : (1 - 1 / (2 * ((D : ℝ) + 1))) * (binaryLength R : ℝ) =
      (binaryLength R : ℝ) - (binaryLength R : ℝ) / (2 * ((D : ℝ) + 1)) := by ring
  rw [hid]
  linarith

theorem binaryLength_rpow_quotient_shrink {R T D : ℕ} {a : ℝ}
    (ha : 0 ≤ a) (hR : D + 1 ≤ Nat.log 2 R)
    (hT : T ≤ R / 2 ^ liftingBits R D) :
    (binaryLength T : ℝ) ^ a ≤ liftingRatio D ^ a * (binaryLength R : ℝ) ^ a := by
  have h := Real.rpow_le_rpow (Nat.cast_nonneg (binaryLength T))
    (binaryLength_quotient_shrink hR hT) ha
  simpa only [Real.mul_rpow (liftingRatio_pos D).le (Nat.cast_nonneg _)] using h

def DyadicModularBounds (a b : ℝ) : Prop :=
  ∃ D k₀ : ℕ, ∃ A B : ℝ, 0 < A ∧ 0 < B ∧
    ∀ k : ℕ, k₀ ≤ k → ∃ F u : ℕ,
      2 ^ k ∣ F.factorial ∧ HasBoundedModularRepresentatives (2 ^ k) F u D ∧
      (F : ℝ) ≤ A * (k : ℝ) ^ a ∧ (u : ℝ) ≤ B * (k : ℝ) ^ b

theorem dyadic_modular_bounds_give_local_multisets {a b : ℝ}
    (ha : 0 < a) (hb : 0 < b) (h : DyadicModularBounds a b) :
    ∃ C E : ℝ, 0 < C ∧ 0 < E ∧ ∀ R : ℕ, 0 < R → ∃ F u : ℕ,