tprod_inv_one_add_real_le_riemannZeta_norm_on_verticalLine

theorem tprod_inv_one_add_real_le_riemannZeta_norm_on_verticalLine (σ t : ℝ) (hσ : 1 < σ) :    ∏' p : Nat.Primes, (1 + ((p : ℕ) : ℝ) ^ (-σ))⁻¹ ≤      ∏' p : Nat.Primes, (‖1 - ((p : ℕ) : ℂ) ^ (-verticalLine σ t)‖)⁻¹ := by  set s := verticalLine σ t  have hs : 1 < s.re := by rw [verticalLine_re]; exact hσ  have hf₀ : ∀ p : Nat.Primes, 0 < (1 + ((p : ℕ) : ℝ) ^ (-σ))⁻¹ := fun _ => by positivity  have hg₀ : ∀ p : Nat.Primes, 0 < (‖1 - ((p : ℕ) : ℂ) ^ (-s)‖)⁻¹ := fun p =>    inv_pos.mpr (norm_pos_iff.mpr (Nat.Primes.one_sub_cpow_neg_vertical_ne_zero p σ t hσ))  let f : Nat.Primes → NNReal := fun p => ⟨(1 + ((p : ℕ) : ℝ) ^ (-σ))⁻¹, (hf₀ p).le⟩  let g : Nat.Primes → NNReal := fun p => ⟨(‖1 - ((p : ℕ) : ℂ) ^ (-s)‖)⁻¹, (hg₀ p).le⟩  have hf := multipliable_toNNReal _ hf₀ <| Nat.Primes.multipliable_inv_one_add σ hσ  have hg := multipliable_toNNReal _ hg₀ <|    multipliable_norm_eulerFactor_inv (g := fun p : Nat.Primes => ((p : ℕ) : ℂ) ^ (-s))      (riemannZeta_eulerProduct_hasProd hs).multipliable  have hle : ∏' p, f p ≤ ∏' p, g p :=    Multipliable.tprod_le_tprod (fun p =>      Nat.Primes.inv_one_add_rpow_le_inv_norm_one_sub_cpow_neg_vertical p σ t hσ) hf hg  calc    ∏' p : Nat.Primes, (1 + ((p : ℕ) : ℝ) ^ (-σ))⁻¹        = ∏' p, (f p : ℝ) := tprod_congr fun p => by unfold f; rfl    _ ≤ ∏' p, (g p : ℝ) := nnreal_tprod_le_coe f g hf hg hle    _ = ∏' p : Nat.Primes, (‖1 - ((p : ℕ) : ℂ) ^ (-s)‖)⁻¹ :=        tprod_congr fun p => by unfold g; rfl