Wkp U e Norm eq zero of ae zero

lemma WkpU.eNorm_eq_zero_of_ae_zero (hp : p ≠ 0) (f : WkpU d k p U hU)    (hf : (↑↑↑f : (Fin d → ℝ) → ℝ) =ᶠ[ae (μU d U)] 0) :    WkpU.eNorm k p f = 0 := by  have h_zero : ∀ n s, WkpU.derivELpNorm f n s = 0 := by    intro n s    cases n with    | zero =>        exact (eLpNorm_congr_ae hf).trans eLpNorm_zero    | succ m =>        dsimp only [WkpU.derivELpNorm]        split_ifs with hnk        · have hweak0 :              (WkpU.weakDeriv f ⟨m+1, Nat.succ_pos _⟩ hnk s)              =ᵐ[μU d U] (0 : (Fin d → ℝ) →ₘ[μU d U] ℝ) := by            apply WeakmultiderivU_unique hU s f.val _ 0            intro ψ hψ            rw [integral_smul_aezero_tsupport hU.measurableSet hf                  (FderivCcinfty s hψ).2.1]            have hint : ∫ x : Fin ↑d → ℝ,                    ψ x • ((0 : ((Fin ↑d → ℝ) →ₘ[μU d U] ℝ)) x) ∂ μU d U = 0 := by              apply integral_eq_zero_of_ae              filter_upwards [AEEqFun.coeFn_zero                  (α := Fin ↑d → ℝ) (μ := μU d U) (β := ℝ)] with x hx              simp [hx]            simpa [smul_eq_mul] using hint          rw [eLpNorm_congr_ae (hweak0.trans AEEqFun.coeFn_zero)]          exact eLpNorm_zero        · rfl  simp only [WkpU.eNorm]  split_ifs with h_top  · simp [h_zero]  · have p_pos : 0 < p.toReal := ENNReal.toReal_pos hp h_top    simp [h_zero, ENNReal.zero_rpow_of_pos p_pos, p_pos]