Erdős problem 12 - part iii

/-
Single-file proof for Erdős problem 12(iii).
The Conjectures.io validator supplies the three imports and opens namespace Bounty.
All local proof dependencies are included below, in dependency order.
Original proof project: the user's chat-log-package/artifacts/lean snapshot.
The internal Erdos12 namespace is renamed to Erdos12Proof to avoid the source statement.
Vendored-source attribution is retained beside each included source.
-/

end Bounty

open scoped Classical


/- BEGIN SOURCE: Erdos12/Basic.lean -/
section
/-
# Property P and its elementary invariances

The convention permits equal larger summands, in which case Property P forces
their equality. It excludes three distinct elements with the least dividing
the sum of the other two. Zero is allowed in the ambient natural-number set.
-/

namespace Erdos12Proof

def PropertyP (A : Set ℕ) : Prop :=
  ∀ ⦃a⦄, a ∈ A → ∀ ⦃b⦄, b ∈ A → ∀ ⦃c⦄, c ∈ A →
    a ∣ b + c → a < b → a < c → b = c

def Primitive (A : Set ℕ) : Prop :=
  ∀ ⦃a⦄, a ∈ A → ∀ ⦃b⦄, b ∈ A → a ∣ b → a = b

def Positive (A : Set ℕ) : Prop := ∀ ⦃a⦄, a ∈ A → 0 < a

abbrev IsGood (A : Set ℕ) : Prop := A.Infinite ∧ PropertyP A

noncomputable def harmonic (B : Finset ℕ) : ℝ := ∑ a ∈ B, (1 / a : ℝ)

theorem PropertyP.mono {A B : Set ℕ} (hA : PropertyP A) (hBA : B ⊆ A) :
    PropertyP B := by
  intro a ha b hb c hc hdiv hab hac
  exact hA (hBA ha) (hBA hb) (hBA hc) hdiv hab hac

theorem Primitive.mono {A B : Set ℕ} (hA : Primitive A) (hBA : B ⊆ A) :
    Primitive B := by
  intro a ha b hb hdiv
  exact hA (hBA ha) (hBA hb) hdiv

theorem PropertyP.dilate {A : Set ℕ} (hA : PropertyP A) {d : ℕ} (hd : 0 < d) :
    PropertyP ((fun n => d * n) '' A) := by
  rintro a ⟨a', ha', rfl⟩ b ⟨b', hb', rfl⟩ c ⟨c', hc', rfl⟩ hdiv hab hac
  have hdiv' : a' ∣ b' + c' := by
    rw [← Nat.mul_add, Nat.mul_dvd_mul_iff_left hd] at hdiv
    exact hdiv
  have heq := hA ha' hb' hc' hdiv'
    ((Nat.mul_lt_mul_left hd).mp hab) ((Nat.mul_lt_mul_left hd).mp hac)
  rw [heq]

theorem PropertyP.of_dilate {A : Set ℕ} {d : ℕ} (hd : 0 < d)
    (hA : PropertyP ((fun n => d * n) '' A)) : PropertyP A := by
  intro a ha b hb c hc hdiv hab hac
  have heq : d * b = d * c := hA ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩ ⟨c, hc, rfl⟩
    (by simpa only [Nat.mul_add] using Nat.mul_dvd_mul_left d hdiv)
    ((Nat.mul_lt_mul_left hd).mpr hab) ((Nat.mul_lt_mul_left hd).mpr hac)
  exact Nat.eq_of_mul_eq_mul_left hd heq

theorem Primitive.of_dilate {A : Set ℕ} {d : ℕ} (hd : 0 < d)
    (hA : Primitive ((fun n => d * n) '' A)) : Primitive A := by
  intro a ha b hb hdiv
  exact Nat.eq_of_mul_eq_mul_left hd
    (hA ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩ (Nat.mul_dvd_mul_left d hdiv))

theorem PropertyP.unique_larger_multiple {A : Set ℕ} (hA : PropertyP A)
    {a b c : ℕ} (ha : a ∈ A) (hb : b ∈ A) (hc : c ∈ A)
    (hab : a < b) (hac : a < c) (hdivb : a ∣ b) (hdivc : a ∣ c) : b = c :=
  hA ha hb hc (dvd_add hdivb hdivc) hab hac

theorem harmonic_nonneg (B : Finset ℕ) : 0 ≤ harmonic B := by
  exact Finset.sum_nonneg (fun a _ => by positivity)

theorem harmonic_mono {B C : Finset ℕ} (hBC : B ⊆ C) : harmonic B ≤ harmonic C := by
  exact Finset.sum_le_sum_of_subset_of_nonneg hBC (fun _ _ _ => by positivity)

end Erdos12Proof
end

/- BEGIN SOURCE: Erdos12/FiniteMean.lean -/
section
/- # Uniform means on finite product spaces -/

namespace Erdos12Proof

section Field

variable {K : Type*} [Field K]

noncomputable def finiteMean {Ω : Type*} [Fintype Ω] (f : Ω → K) : K :=
  (∑ x, f x) / Fintype.card Ω

theorem finiteMean_const [CharZero K] {Ω : Type*} [Fintype Ω] [Nonempty Ω] (c : K) :
    finiteMean (fun _ : Ω => c) = c := by
  unfold finiteMean
  simp [Fintype.card_ne_zero]

theorem finiteMean_zero {Ω : Type*} [Fintype Ω] :
    finiteMean (fun _ : Ω => (0 : K)) = 0 := by
  simp [finiteMean]

theorem finiteMean_add {Ω : Type*} [Fintype Ω] (f g : Ω → K) :
    finiteMean (fun x => f x + g x) = finiteMean f + finiteMean g := by
  simp only [finiteMean, Finset.sum_add_distrib, add_div]

theorem finiteMean_mul_const {Ω : Type*} [Fintype Ω] (f : Ω → K) (c : K) :
    finiteMean (fun x => f x * c) = finiteMean f * c := by
  simp only [finiteMean, ← Finset.sum_mul]
  ring

theorem finiteMean_const_mul {Ω : Type*} [Fintype Ω] (c : K) (f : Ω → K) :
    finiteMean (fun x => c * f x) = c * finiteMean f := by
  simp only [finiteMean, ← Finset.mul_sum]
  ring

theorem finiteMean_sum {Ω ι : Type*} [Fintype Ω] (s : Finset ι) (f : ι → Ω → K) :
    finiteMean (fun x => ∑ i ∈ s, f i x) = ∑ i ∈ s, finiteMean (f i) := by
  simp only [finiteMean, Finset.sum_div]
  rw [Finset.sum_comm]

theorem finiteMean_prod {ι : Type*} [Fintype ι] [DecidableEq ι]
    {Ω : ι → Type*} [∀ i, Fintype (Ω i)] (f : ∀ i, Ω i → K) :
    finiteMean (fun x : ∀ i, Ω i => ∏ i, f i (x i)) = ∏ i, finiteMean (f i) := by
  unfold finiteMean
  rw [← Fintype.prod_sum, Finset.prod_div_distrib, Fintype.card_pi]
  simp only [Nat.cast_prod]

end Field

theorem finiteMean_nonneg {Ω : Type*} [Fintype Ω] {f : Ω → ℝ} (hf : ∀ x, 0 ≤ f x) :
    0 ≤ finiteMean f := by
  exact div_nonneg (Finset.sum_nonneg (fun x _ => hf x)) (Nat.cast_nonneg _)

theorem finiteMean_mono {Ω : Type*} [Fintype Ω] {f g : Ω → ℝ} (h : ∀ x, f x ≤ g x) :
    finiteMean f ≤ finiteMean g := by
  exact div_le_div_of_nonneg_right (Finset.sum_le_sum (fun x _ => h x)) (Nat.cast_nonneg _)

end Erdos12Proof
end

/- BEGIN SOURCE: Erdos12/FiniteProductWeights.lean -/
section
/- # Explicit probability weights on finite product spaces -/

namespace Erdos12Proof

variable {ι : Type*} [Fintype ι] [DecidableEq ι]
variable {Ω : ι → Type*} [∀ i, Fintype (Ω i)]

noncomputable def productWeight (w : ∀ i, Ω i → ℝ) (ω : ∀ i, Ω i) : ℝ :=
  ∏ i, w i (ω i)

omit [DecidableEq ι] [∀ i, Fintype (Ω i)] in
theorem productWeight_nonneg (w : ∀ i, Ω i → ℝ) (hw : ∀ i x, 0 ≤ w i x) (ω : ∀ i, Ω i) :
    0 ≤ productWeight w ω := Finset.prod_nonneg (fun i _ => hw i (ω i))

theorem productWeight_sum (w : ∀ i, Ω i → ℝ) :
    (∑ ω : ∀ i, Ω i, productWeight w ω) = ∏ i, ∑ x, w i x := by
  unfold productWeight
  rw [← Fintype.prod_sum]

theorem productWeight_mass (w : ∀ i, Ω i → ℝ) (hw : ∀ i, (∑ x, w i x) = 1) :
    (∑ ω : ∀ i, Ω i, productWeight w ω) = 1 := by
  rw [productWeight_sum]
  simp only [hw, Finset.prod_const_one]

theorem productWeight_factorization (w f : ∀ i, Ω i → ℝ) :
    (∑ ω : ∀ i, Ω i, productWeight w ω * ∏ i, f i (ω i)) =
      ∏ i, ∑ x, w i x * f i x := by
  simp only [productWeight, ← Finset.prod_mul_distrib]
  exact (Fintype.prod_sum (fun i x => w i x * f i x)).symm

theorem productWeight_restricted_sum (w : ∀ i, Ω i → ℝ) (P : ∀ i, Ω i → Prop)
    [∀ i, DecidablePred (P i)] :
    (∑ ω : ∀ i, Ω i, if ∀ i, P i (ω i) then productWeight w ω else 0) =
      ∏ i, ∑ x, if P i x then w i x else 0 := by
  classical
  have hpoint (ω : ∀ i, Ω i) :
      (if ∀ i, P i (ω i) then productWeight w ω else 0) =
        ∏ i, if P i (ω i) then w i (ω i) else 0 := by
    by_cases h : ∀ i, P i (ω i)
    · rw [ite_eq_left h]
      unfold productWeight
      apply Finset.prod_congr rfl
      intro i _
      rw [ite_eq_left (h i)]
    · rw [ite_eq_right h]
      obtain ⟨i, hi⟩ := not_forall.mp h
      symm
      exact Finset.prod_eq_zero (Finset.mem_univ i) (ite_eq_right hi)
  simp only [hpoint]
  exact (Fintype.prod_sum (fun i x => if P i x then w i x else 0)).symm

noncomputable def weightedSum {X : Type*} [Fintype X] (w f : X → ℝ) : ℝ :=
  ∑ x, w x * f x

theorem weightedSum_mono {X : Type*} [Fintype X] (w : X → ℝ) (hw : ∀ x, 0 ≤ w x)
    {f g : X → ℝ} (hfg : ∀ x, f x ≤ g x) : weightedSum w f ≤ weightedSum w g :=
  Finset.sum_le_sum (fun x _ => mul_le_mul_of_nonneg_left (hfg x) (hw x))

theorem weightedSum_finite_sum {X κ : Type*} [Fintype X] (w : X → ℝ)
    (S : Finset κ) (f : κ → X → ℝ) :
    weightedSum w (fun x => ∑ i ∈ S, f i x) = ∑ i ∈ S, weightedSum w (f i) := by
  simp only [weightedSum, Finset.mul_sum]
  rw [Finset.sum_comm]

end Erdos12Proof
end

/- BEGIN SOURCE: Erdos12/FiniteCoordinateWeights.lean -/
section
/- # Conditional factorization at one finite product coordinate -/

namespace Erdos12Proof

variable {ι : Type*} [Fintype ι] [DecidableEq ι]
variable {Ω : ι → Type*} [∀ i, Fintype (Ω i)]

omit [∀ i, Fintype (Ω i)] in
theorem productWeight_splitAt (w : ∀ i, Ω i → ℝ) (i : ι) (x : Ω i)
    (r : ∀ j : {j // j ≠ i}, Ω j) :
    productWeight w ((Equiv.piSplitAt i Ω).symm (x, r)) =
      w i x * productWeight (fun j : {j // j ≠ i} => w j.val) r := by
  unfold productWeight
  rw [Fintype.prod_eq_mul_prod_subtype_ne _ i]
  have hcoord : (Equiv.piSplitAt i Ω).symm (x, r) i = x := by simp [Equiv.piSplitAt]
  rw [hcoord]
  congr 1
  apply Finset.prod_congr rfl
  intro j _
  simp [Equiv.piSplitAt, j.property]

theorem weightedSum_splitAt (w : ∀ i, Ω i → ℝ) (F : (∀ i, Ω i) → ℝ) (i : ι) :
    weightedSum (productWeight w) F = ∑ x : Ω i, w i x *
      ∑ r : (∀ j : {j // j ≠ i}, Ω j),
        productWeight (fun j : {j // j ≠ i} => w j.val) r * F ((Equiv.piSplitAt i Ω).symm (x, r)) := by
  classical
  unfold weightedSum
  rw [← (Equiv.piSplitAt i Ω).symm.sum_comp
    (fun ω => productWeight w ω * F ω), Fintype.sum_prod_type]
  simp only [productWeight_splitAt, Finset.mul_sum, mul_assoc]

theorem weightedSum_coordinate_pairing (w : ∀ i, Ω i → ℝ) (i : ι) [Nonempty (Ω i)]
    (hw : (∑ x, w i x) = 1) (g : Ω i → ℝ) (F : (∀ i, Ω i) → ℝ)
    (hF : ∀ ω x, F (Function.update ω i x) = F ω) :
    weightedSum (productWeight w) (fun ω => g (ω i) * F ω) =
      (∑ x, w i x * g x) * weightedSum (productWeight w) F := by
  classical
  let x₀ : Ω i := Classical.choice ‹Nonempty (Ω i)›
  let e := Equiv.piSplitAt i Ω
  let V := ∑ r : (∀ j : {j // j ≠ i}, Ω j),
    productWeight (fun j : {j // j ≠ i} => w j.val) r * F (e.symm (x₀, r))
  have hcoord (x : Ω i) (r : ∀ j : {j // j ≠ i}, Ω j) : e.symm (x, r) i = x := by
    simp [e, Equiv.piSplitAt]
  have hsame (x : Ω i) (r : ∀ j : {j // j ≠ i}, Ω j) : F (e.symm (x, r)) = F (e.symm (x₀, r)) := by
    have heq : e.symm (x, r) = Function.update (e.symm (x₀, r)) i x := by
      funext j
      by_cases hji : j = i
      · subst j
        simp [hcoord]
      · simp [e, Equiv.piSplitAt, hji]
    rw [heq, hF]
  have hbase : weightedSum (productWeight w) F = V := by
    rw [weightedSum_splitAt w F i]
    change (∑ x : Ω i, w i x * ∑ r, productWeight (fun j : {j // j ≠ i} => w j.val) r *
      F (e.symm (x, r))) = V
    simp_rw [hsame]
    change (∑ x : Ω i, w i x * V) = V
    rw [← Finset.sum_mul, hw, one_mul]
  rw [hbase, weightedSum_splitAt w (fun ω => g (ω i) * F ω) i]
  change (∑ x : Ω i, w i x * ∑ r, productWeight (fun j : {j // j ≠ i} => w j.val) r *
    (g (e.symm (x, r) i) * F (e.symm (x, r)))) = _
  simp_rw [hcoord, hsame]
  calc
    _ = ∑ x : Ω i, (w i x * g x) * V := by
      apply Finset.sum_congr rfl
      intro x _
      dsimp only [V]
      rw [Finset.mul_sum, Finset.mul_sum]
      apply Finset.sum_congr rfl
      intro r _
      ring
    _ = _ := (Finset.sum_mul _ _ _).symm

end Erdos12Proof
end

/- BEGIN SOURCE: Erdos12/GeometricWeights.lean -/
section
/-
# Exact geometric weights used by the prefix argument

The parameter is the prime value itself. The following identities hold for
every real parameter greater than one, so primality is unnecessary here.
-/

namespace Erdos12Proof

noncomputable def geometricWeight (p : ℝ) (j : ℕ) : ℝ :=
  (1 - 1 / p) * (1 / p) ^ j

theorem geometric_ratio_bounds {p : ℝ} (hp : 1 < p) :
    0 ≤ 1 / p ∧ 1 / p < 1 := by
  have hp0 : 0 < p := lt_trans zero_lt_one hp
  exact ⟨le_of_lt (one_div_pos.mpr hp0), (div_lt_one hp0).mpr hp⟩

theorem geometricWeight_nonneg {p : ℝ} (hp : 1 < p) (j : ℕ) :
    0 ≤ geometricWeight p j := by
  obtain ⟨h0, h1⟩ := geometric_ratio_bounds hp
  exact mul_nonneg (sub_nonneg.mpr h1.le) (pow_nonneg h0 j)

theorem hasSum_geometricWeight {p : ℝ} (hp : 1 < p) :
    HasSum (geometricWeight p) 1 := by
  obtain ⟨h0, h1⟩ := geometric_ratio_bounds hp
  have hs := (hasSum_geometric_of_lt_one h0 h1).mul_left (1 - 1 / p)
  convert hs using 1
  · rfl
  · have hne : 1 - 1 / p ≠ 0 := ne_of_gt (sub_pos.mpr h1)
    exact (mul_inv_cancel₀ hne).symm

theorem hasSum_geometricWeight_tail {p : ℝ} (hp : 1 < p) (k : ℕ) :
    HasSum (fun j => geometricWeight p (j + k)) ((1 / p) ^ k) := by
  have hs := (hasSum_geometricWeight hp).mul_right ((1 / p) ^ k)
  convert hs using 1
  · funext j
    simp only [geometricWeight, pow_add]
    ring
  · ring

theorem hasSum_repeated_copy_cost {p : ℝ} (hp : 1 < p) :
    HasSum (fun j : ℕ => (j : ℝ) * geometricWeight p (j + 1)) (1 / (p * (p - 1))) := by
  obtain ⟨h0, h1⟩ := geometric_ratio_bounds hp
  have hnorm : ‖1 / p‖ < 1 := by rwa [Real.norm_eq_abs, abs_of_nonneg h0]
  have hs := (hasSum_descFactorial_mul_geometric_of_norm_lt_one
    (𝕜 := ℝ) 1 hnorm).mul_left ((1 - 1 / p) * (1 / p))
  convert hs using 1
  · funext j
    simp only [geometricWeight, Nat.descFactorial_one, pow_succ]
    ring
  · norm_num
    have hp0 : p ≠ 0 := ne_of_gt (lt_trans zero_lt_one hp)
    have hp1 : p - 1 ≠ 0 := ne_of_gt (sub_pos.mpr hp)
    field_simp

theorem hasSum_stage_budget :
    HasSum (fun k : ℕ => (1 / 2 : ℝ) ^ k * (1 + (k : ℝ))) 4 := by
  have h0 : ‖(1 / 2 : ℝ)‖ < 1 := by norm_num
  have hs0 := hasSum_geometric_of_norm_lt_one h0
  have hs1 := hasSum_descFactorial_mul_geometric_of_norm_lt_one (𝕜 := ℝ) 1 h0
  have hs := hs0.add hs1
  convert hs using 1
  · funext k
    simp only [Nat.descFactorial_one]
    ring
  · norm_num

end Erdos12Proof
end

/- BEGIN SOURCE: Erdos12/TruncatedGeometric.lean -/
section
/- # Finite geometric distributions with the tail collected at the last value -/

namespace Erdos12Proof

theorem sum_geometricWeight_range (p : ℝ) (N : ℕ) :
    (∑ j ∈ Finset.range N, geometricWeight p j) = 1 - (1 / p) ^ N := by
  have h := geom_sum_mul (1 / p : ℝ) N
  unfold geometricWeight
  rw [← Finset.mul_sum]
  nlinarith

noncomputable def truncatedGeometricWeight (p : ℝ) (cap : ℕ) (j : Fin (cap + 1)) : ℝ :=
  if j.val < cap then geometricWeight p j.val else (1 / p) ^ cap

theorem truncatedGeometricWeight_nonneg {p : ℝ} (hp : 1 < p) (cap : ℕ) (j : Fin (cap + 1)) :
    0 ≤ truncatedGeometricWeight p cap j := by
  unfold truncatedGeometricWeight
  split_ifs
  · exact geometricWeight_nonneg hp _
  · exact pow_nonneg (geometric_ratio_bounds hp).1 _

theorem truncatedGeometricWeight_below {cap : ℕ} (p : ℝ) (j : Fin (cap + 1)) (hj : j.val < cap) :
    truncatedGeometricWeight p cap j = geometricWeight p j.val := by
  exact ite_eq_left hj

theorem truncatedGeometricWeight_last (p : ℝ) (cap : ℕ) :
    truncatedGeometricWeight p cap (Fin.last cap) = (1 / p) ^ cap := by
  simp only [truncatedGeometricWeight, Fin.val_last, lt_self_iff_false, ite_false]

theorem truncatedGeometricWeight_sum (p : ℝ) (cap : ℕ) :
    (∑ j : Fin (cap + 1), truncatedGeometricWeight p cap j) = 1 := by
  rw [Fin.sum_univ_castSucc]
  have hbelow (j : Fin cap) : truncatedGeometricWeight p cap j.castSucc = geometricWeight p j.val :=
    truncatedGeometricWeight_below p j.castSucc j.isLt
  simp only [hbelow, truncatedGeometricWeight_last]
  rw [Fin.sum_univ_eq_sum_range, sum_geometricWeight_range]
  ring

theorem truncatedGeometricWeight_tail (p : ℝ) (cap a : ℕ) (ha : a ≤ cap) :
    (∑ j : Fin (cap + 1), if a ≤ j.val then truncatedGeometricWeight p cap j else 0) =
      (1 / p) ^ a := by
  have hsplit := Finset.sum_filter_add_sum_filter_not (Finset.univ : Finset (Fin (cap + 1)))
    (fun j => j.val < a) (truncatedGeometricWeight p cap)
  have hlow : (∑ j ∈ (Finset.univ : Finset (Fin (cap + 1))).filter (fun j => j.val < a),
      truncatedGeometricWeight p cap j) = 1 - (1 / p) ^ a := by
    calc
      _ = ∑ j ∈ Finset.range a, geometricWeight p j := by
        apply Finset.sum_bij (fun j _ => j.val)
        · intro j hj
          exact Finset.mem_range.mpr (Finset.mem_filter.mp hj).2
        · intro i _ j _ hij
          exact Fin.ext hij
        · intro j hj
          refine ⟨⟨j, by have := Finset.mem_range.mp hj; omega⟩, ?_, rfl⟩
          exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, Finset.mem_range.mp hj⟩
        · intro j hj
          exact truncatedGeometricWeight_below p j ((Finset.mem_filter.mp hj).2.trans_le ha)
      _ = _ := sum_geometricWeight_range p a
  rw [hlow, truncatedGeometricWeight_sum] at hsplit
  have hhigh : (∑ j : Fin (cap + 1), if a ≤ j.val then truncatedGeometricWeight p cap j else 0) =
      ∑ j ∈ (Finset.univ : Finset (Fin (cap + 1))).filter (fun j => ¬j.val < a),
        truncatedGeometricWeight p cap j := by
    rw [Finset.sum_filter]
    simp only [not_lt]
  rw [hhigh]
  linarith

end Erdos12Proof
end

/- BEGIN SOURCE: Erdos12/FiniteGeometricProbability.lean -/
section
/- # Finite geometric product probabilities and predictable-coordinate identities -/

namespace Erdos12Proof

theorem truncatedGeometricWeight_atom (p : ℝ) (cap a : ℕ) (ha : a < cap) :
    (∑ x : Fin (cap + 1), if x.val = a then truncatedGeometricWeight p cap x else 0) =
      geometricWeight p a := by
  classical
  let x : Fin (cap + 1) := ⟨a, by omega⟩
  have hcond (y : Fin (cap + 1)) : y.val = a ↔ y = x := by
    exact ⟨fun h => Fin.ext h, fun h => congrArg Fin.val h⟩
  simp only [hcond, Finset.sum_ite_eq', Finset.mem_univ, ite_true]
  exact truncatedGeometricWeight_below p x ha

variable {ι : Type*} [Fintype ι] [DecidableEq ι]

noncomputable def finiteGeometricProductWeight (p : ι → ℝ) (cap : ℕ)
    (ω : ι → Fin (cap + 1)) : ℝ :=
  productWeight (fun i => truncatedGeometricWeight (p i) cap) ω

theorem finiteGeometricProductWeight_mass (p : ι → ℝ) (cap : ℕ) :
    (∑ ω : ι → Fin (cap + 1), finiteGeometricProductWeight p cap ω) = 1 :=
  productWeight_mass _ (fun i => truncatedGeometricWeight_sum (p i) cap)

omit [DecidableEq ι] in
theorem finiteGeometricProductWeight_nonneg (p : ι → ℝ) (hp : ∀ i, 1 < p i)
    (cap : ℕ) (ω : ι → Fin (cap + 1)) : 0 ≤ finiteGeometricProductWeight p cap ω :=
  productWeight_nonneg _ (fun i x => truncatedGeometricWeight_nonneg (hp i) cap x) ω

theorem finiteGeometric_tail_pairing (p : ι → ℝ) (cap : ℕ) (i : ι) (a : ℕ) (ha : a ≤ cap)
    (F : (ι → Fin (cap + 1)) → ℝ)
    (hF : ∀ ω x, F (Function.update ω i x) = F ω) :
    weightedSum (finiteGeometricProductWeight p cap)
      (fun ω => if a ≤ (ω i).val then F ω else 0) =
        (1 / p i) ^ a * weightedSum (finiteGeometricProductWeight p cap) F := by
  have h := weightedSum_coordinate_pairing (fun i => truncatedGeometricWeight (p i) cap) i
    (truncatedGeometricWeight_sum (p i) cap) (fun x => if a ≤ x.val then 1 else 0) F hF
  have hlocal : (∑ x : Fin (cap + 1), truncatedGeometricWeight (p i) cap x *
      (if a ≤ x.val then 1 else 0)) = (1 / p i) ^ a := by
    simp only [mul_ite, mul_one, mul_zero]
    exact truncatedGeometricWeight_tail (p i) cap a ha
  rw [hlocal] at h
  simpa only [weightedSum, finiteGeometricProductWeight, ite_mul, one_mul, zero_mul] using h

end Erdos12Proof
end

/- BEGIN SOURCE: Erdos12/SelbergTensor.lean -/
section
/- # Orthogonal products underlying the Selberg majorant -/

namespace Erdos12Proof

variable {ι : Type*} [Fintype ι] [DecidableEq ι]
variable {Ω : ι → Type*}

noncomputable def tensorBasis (u : ∀ i, Ω i → ℝ) (s : Finset ι) (x : ∀ i, Ω i) : ℝ :=
  ∏ i, if i ∈ s then u i (x i) else 1