Wkp U tendsto iff all deriv ELp Norm

lemma WkpU.tendsto_iff_all_derivELpNorm    [Fact (1 ≤ p)] {fₙ : ℕ → WkpU d k p U hU} {f : WkpU d k p U hU} :    Tendsto fₙ atTop (𝓝 f) ↔      ∀ (n : Fin (k + 1)) (s : Fin n.val → Fin d),        Tendsto (fun j => WkpU.derivELpNorm (fₙ j - f) n.val s) atTop (𝓝 0) := by  rw [← tendsto_sub_nhds_zero_iff, tendsto_iff_norm_sub_tendsto_zero]; simp only [sub_zero]  have hle : ∀ (g : WkpU d k p U hU) (n : Fin (k + 1)) (s : Fin n.val → Fin d),      (WkpU.derivELpNorm g n.val s).toReal ≤ ‖g‖ := fun g n s =>    (ENNReal.toNNReal_le_toNNReal (WkpU.derivELpNorm_ne_top g n s) (WkpU.eNorm_ne_top g)).mpr <| by      rcases n with ⟨m, hm⟩; cases m with      | zero   => exact WkpU.derivELpNorm_zero_le_eNorm g      | succ m => exact WkpU.derivELpNorm_le_eNorm g ⟨m+1, Nat.succ_pos m⟩ (Nat.lt_succ_iff.mp hm) s  have hnorm : ∀ (g : WkpU d k p U hU), ‖g‖ ≤      ∑ n : Fin (k+1), ∑ s : Fin n.val → Fin d, (WkpU.derivELpNorm g n.val s).toReal := by    intro g    show (WkpU.eNorm k p g).toReal ≤ _    simp only [WkpU.eNorm]    split_ifs with hp_top    · have hmono := ENNReal.toReal_mono        (ENNReal.sum_ne_top.mpr fun n _ => ENNReal.sum_ne_top.mpr fun s _ =>          WkpU.derivELpNorm_ne_top g n s)        (iSup_le fun n => iSup_le fun s =>          (Finset.single_le_sum (f := fun s' : Fin n.val → Fin ↑d => WkpU.derivELpNorm g n.val s')            (fun _ _ => zero_le) (Finset.mem_univ s)).trans          (Finset.single_le_sum (f := fun n' : Fin (k+1) =>            ∑ s' : Fin n'.val → Fin ↑d, WkpU.derivELpNorm g n'.val s')            (fun _ _ => Finset.sum_nonneg fun _ _ => zero_le) (Finset.mem_univ n)))      simp_rw [ENNReal.toReal_sum (fun n _ => ENNReal.sum_ne_top.mpr fun s _ =>          WkpU.derivELpNorm_ne_top g n s),        ENNReal.toReal_sum (fun s _ => WkpU.derivELpNorm_ne_top g _ s)] at hmono; exact hmono    · have hp1 : 1 ≤ p.toReal := ENNReal.toReal_mono hp_top (Fact.out : 1 ≤ p)      have hp_pos : 0 < p.toReal := lt_of_lt_of_le zero_lt_one hp1      rw [← ENNReal.toReal_rpow, ENNReal.toReal_sum (fun n _ => ENNReal.sum_ne_top.mpr fun s _ =>          ENNReal.rpow_ne_top_of_nonneg hp_pos.le (WkpU.derivELpNorm_ne_top g n s))]      simp_rw [ENNReal.toReal_sum (fun s _ => ENNReal.rpow_ne_top_of_nonneg hp_pos.le          (WkpU.derivELpNorm_ne_top g _ s)), ← ENNReal.toReal_rpow]      haveI : Nonempty (Σ n : Fin (k+1), Fin n.val → Fin ↑d) := ⟨⟨⟨0, k.succ_pos⟩, Fin.elim0⟩⟩      let e := Fintype.equivFin (Σ n : Fin (k + 1), Fin n.val → Fin ↑d)      rw [(Fintype.sum_sigma (fun i : Σ n : Fin (k+1), Fin n.val → Fin ↑d =>              (WkpU.derivELpNorm g i.1.val i.2).toReal ^ p.toReal)).symm,          (Fintype.sum_sigma (fun i : Σ n : Fin (k+1), Fin n.val → Fin ↑d =>              (WkpU.derivELpNorm g i.1.val i.2).toReal)).symm,          ← e.symm.sum_comp _, ← e.symm.sum_comp _]      exact NNReal.rpow_sum_le_sum hp1 _ Fintype.card_pos        (fun j => ⟨(WkpU.derivELpNorm g (e.symm j).1.val (e.symm j).2).toReal,                    ENNReal.toReal_nonneg⟩)  constructor  · intro h n s    have hreal : Tendsto (fun j =>          (WkpU.derivELpNorm (fₙ j - f) n.val s).toReal) atTop (𝓝 0) :=        squeeze_zero (fun _ => ENNReal.toReal_nonneg)          (fun j => by exact_mod_cast hle (fₙ j - f) n s) h    simpa [ENNReal.ofReal_toReal (WkpU.derivELpNorm_ne_top _ n s)] using        ENNReal.tendsto_ofReal hreal  · intro h    refine squeeze_zero (fun j => norm_nonneg _) (fun j => hnorm (fₙ j - f)) ?_    simpa using tendsto_finsetSum Finset.univ fun n _ =>      tendsto_finsetSum Finset.univ fun s _ =>        (ENNReal.tendsto_toReal zero_ne_top).comp (h n s)