Dlog Success sq le cdh Success dlog To CDHReduction

theorem dlogSuccess_sq_le_cdhSuccess_dlogToCDHReduction    (g : G) (adversary : DLogAdversary F G) :    (Pr[= true | dlogExp g adversary]).toReal ^ 2 ≤      (Pr[= true | cdhExp g (dlogToCDHReduction (F := F) adversary)]).toReal := by  rw [← ENNReal.toReal_pow]  refine ENNReal.toReal_mono probOutput_ne_top ?_  set w : F → ℝ≥0∞ := fun x => Pr[= x | $ᵗ F]  set f : F → ℝ≥0∞ := fun x => Pr[= x | adversary g (x • g)]  rw [sq, dlogExp_probOutput_eq_tsum, ← ENNReal.tsum_mul_right,    cdhExp_dlogToCDHReduction_probOutput_eq_tsum]  refine ENNReal.tsum_le_tsum fun a => ?_  rw [← ENNReal.tsum_mul_left]  refine ENNReal.tsum_le_tsum fun b => ?_  calc w a * f a * (w b * f b)      = w a * (w b * (f a * (f b * (if (a * b) • g = (a * b) • g then 1 else 0)))) := by        simp only [if_true, mul_one]        ring    _ ≤ ∑' (b' : F), w a * (w b * (f a *          (Pr[= b' | adversary g (b • g)] *            (if (a * b') • g = (a * b) • g then 1 else 0)))) := ENNReal.le_tsum b    _ ≤ ∑' (a' : F) (b' : F), w a * (w b * (Pr[= a' | adversary g (a • g)] *          (Pr[= b' | adversary g (b • g)] *            (if (a' * b') • g = (a * b) • g then 1 else 0)))) := ENNReal.le_tsum a