Doubly stochastic holder

lemma doubly_stochastic_holder (a b : d → ℝ) (w : d → d → ℝ)    (ha : ∀ i, 0 ≤ a i) (hb : ∀ j, 0 ≤ b j)    (hw : ∀ i j, 0 ≤ w i j)    (hrow : ∀ i, ∑ j, w i j = 1) (hcol : ∀ j, ∑ i, w i j = 1)    (p q : ℝ) (hp : 1 < p) (hpq : 1/p + 1/q = 1) :    ∑ i, ∑ j, a i * b j * w i j ≤ (∑ i, a i ^ p) ^ (1/p) * (∑ j, b j ^ q) ^ (1/q) := by  by_contra h_contra  contrapose! h_contra with h_contra  simp_all [ ← Finset.mul_sum, mul_assoc ]  have h0q : 0 < q :=    lt_of_le_of_ne ( le_of_not_gt fun hq => by { rw [ inv_eq_one_div, div_eq_mul_inv ] at hpq; nlinarith [ inv_mul_cancel₀ ( by linarith : ( p : ℝ ) ≠ 0 ), inv_lt_zero.2 hq ] } ) (by grind)  -- Apply Hölder's inequality with the sequences $a_i$ and $g_i = \sum_j w_{ij} b_j$.  have h_holder : (∑ i, a i * (∑ j, w i j * b j)) ≤ (∑ i, a i ^ p) ^ (1 / p) * (∑ i, (∑ j, w i j * b j) ^ q) ^ (1 / q) := by    have := @Real.inner_le_Lp_mul_Lq    simp_all    convert this Finset.univ a ( fun i => ∑ j, w i j * b j ) ( show p.HolderConjugate q from ?_ ) using 1    · simp only [ha, abs_of_nonneg, mul_eq_mul_left_iff]      left      congr!      symm      exact abs_of_nonneg (Finset.sum_nonneg fun _ _ ↦ mul_nonneg (hw _ _) (hb _))    · constructor <;> linarith  -- By Fubini's theorem, we can interchange the order of summation.  have h_fubini : ∑ i, (∑ j, w i j * b j) ^ q ≤ ∑ j, b j ^ q := by    -- Apply Jensen's inequality to the convex function $x^q$ with weights $w_{ij}$.    have h_jensen : ∀ i, (∑ j, w i j * b j) ^ q ≤ ∑ j, w i j * b j ^ q := by      intro i      have h_jensen : ConvexOn ℝ (Set.Ici 0) (fun x : ℝ => x ^ q) := by        apply convexOn_rpow        nlinarith [ inv_pos.2 ( zero_lt_one.trans hp ), inv_pos.2 h0q, mul_inv_cancel₀ h0q.ne']      convert h_jensen.map_sum_le _ _ _ <;> aesop    refine' le_trans ( Finset.sum_le_sum fun i _ => h_jensen i ) _;    rw [ Finset.sum_comm ]    simp [ ← Finset.sum_mul, hcol]  simp_all only [mul_comm];  simpa using h_holder.trans ( mul_le_mul_of_nonneg_left ( Real.rpow_le_rpow ( Finset.sum_nonneg fun _ _ => Real.rpow_nonneg ( Finset.sum_nonneg fun _ _ => mul_nonneg ( hb _ ) ( hw _ _ ) ) _ ) h_fubini (one_div_nonneg.mpr h0q.le)) ( Real.rpow_nonneg ( Finset.sum_nonneg fun _ _ => Real.rpow_nonneg ( ha _ ) _ ) _ ) ) |> le_trans <| by simp;