∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {p q : ENNReal},
  p.toReal.HolderConjugate q.toReal → ∀ (f : ↥(lp E p)) (g : ↥(lp E q)), Summable fun i => ‖↑f i‖ * ‖↑g i‖