Ae eq zero of mem H01 of grad Lp Of Witness eq zero

theorem ae_eq_zero_of_memH01_of_gradLpOfWitness_eq_zero    {Ω : Set E} (hd : 2 ≤ d) (hΩ : IsOpen Ω)    (hΩ_bdd : Bornology.IsBounded Ω)    {u : E → ℝ}    (hu0 : MemH01 u Ω)    (hwu : MemW1pWitness 2 u Ω)    (hgrad_zero : gradLpOfWitness hwu = 0) :    u =ᵐ[volume.restrict Ω] 0 := by  let μ : Measure E := volume.restrict Ω  obtain ⟨hu_mem, hw0, φ, hφ_smooth, hφ_cpt, hφ_sub, hφ_fun, hφ_grad⟩ := hu0  have hgrad_ae :      hw0.weakGrad =ᵐ[μ] hwu.weakGrad := by    simpa [μ] using MemW1pWitness.ae_eq hΩ hw0 hwu  have hgradLp_eq : gradLpOfWitness hw0 = gradLpOfWitness hwu := by    simpa [gradLpOfWitness] using      (MemLp.toLp_congr hw0.weakGrad_memLp hwu.weakGrad_memLp hgrad_ae)  have hgrad_zero0 : gradLpOfWitness hw0 = 0 := by    rw [hgradLp_eq]    exact hgrad_zero  let hφtest : ∀ n : ℕ, IsSmoothTestOn Ω (φ n) := fun n =>    ⟨hφ_smooth n, hφ_cpt n, hφ_sub n⟩  let hφw : ∀ n : ℕ, MemW1pWitness 2 (φ n) Ω := fun n =>    smoothTestWitness hΩ (hφtest n)  have hφ_fun_tendsto :      Tendsto (fun n => smoothFunToLp hΩ (hφtest n))        atTop (nhds (hu_mem.1.toLp u)) := by    exact      (Lp.tendsto_Lp_iff_tendsto_eLpNorm'' (f := φ)        (f_ℒp := fun n => (hφw n).memLp)        (f_lim := u) (f_lim_ℒp := hu_mem.1)).2 <| by          simpa [μ] using hφ_fun  have hgrad_vec_tendsto :      Tendsto        (fun n => eLpNorm (fun x => (hφw n).weakGrad x - hw0.weakGrad x) 2 μ)        atTop (nhds 0) := by    exact tendsto_eLpNorm_vector_of_componentwise      (fun n i => by        simpa [hφw] using ((hφw n).weakGrad_component_memLp i).sub (hw0.weakGrad_component_memLp i))      (fun i => by simpa [μ] using hφ_grad i)  have hgradLp_tendsto :      Tendsto (fun n => gradLpOfWitness (hφw n))        atTop (nhds (gradLpOfWitness hw0)) := by    exact      (Lp.tendsto_Lp_iff_tendsto_eLpNorm'' (f := fun n => (hφw n).weakGrad)        (f_ℒp := fun n => (hφw n).weakGrad_memLp)        (f_lim := hw0.weakGrad) (f_lim_ℒp := hw0.weakGrad_memLp)).2        hgrad_vec_tendsto  have hgradLp_zero_tendsto :      Tendsto (fun n => gradLpOfWitness (hφw n)) atTop (nhds 0) := by    simpa [hgrad_zero0] using hgradLp_tendsto  obtain ⟨Cp, hCp_top, hPoinc⟩ := smoothCompactSupport_L2_bound_on_bounded_ge_two hd hΩ_bdd  have hfun_bound :      ∀ n, ‖smoothFunToLp hΩ (hφtest n)‖ ≤ Cp.toReal * ‖smoothGradToLp hΩ (hφtest n)‖ := by    intro n    have hgradNorm_memLp : MemLp (smoothGradNorm (φ n)) 2 μ := by      simpa [μ, norm_smoothGradField_eq_smoothGradNorm] using (hφw n).weakGrad_memLp.norm    have hP :        eLpNorm (φ n) 2 μ ≤ Cp * eLpNorm (smoothGradNorm (φ n)) 2 μ := by      simpa [μ] using hPoinc (hφ_smooth n) (hφ_cpt n) (hφ_sub n)    have hleft_top : eLpNorm (φ n) 2 μ ≠ ⊤ := (hφw n).memLp.eLpNorm_lt_top.ne    have hright_top : Cp * eLpNorm (smoothGradNorm (φ n)) 2 μ ≠ ⊤ := by      exact (ENNReal.mul_lt_top hCp_top hgradNorm_memLp.eLpNorm_lt_top).ne    have hToReal :        (eLpNorm (φ n) 2 μ).toReal ≤ (Cp * eLpNorm (smoothGradNorm (φ n)) 2 μ).toReal :=      (ENNReal.toReal_le_toReal hleft_top hright_top).2 hP    have hfunEq : ‖smoothFunToLp hΩ (hφtest n)‖ = (eLpNorm (φ n) 2 μ).toReal := by      rw [smoothFunToLp, Lp.norm_toLp]    have hgradEq : ‖smoothGradToLp hΩ (hφtest n)‖ = (eLpNorm (smoothGradNorm (φ n)) 2 μ).toReal := by      have hgrad_memLp : MemLp (smoothGradField (φ n)) 2 μ := (hφw n).weakGrad_memLp      calc        ‖smoothGradToLp hΩ (hφtest n)‖            = (∫ x, ‖smoothGradField (φ n) x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) := by                simpa [μ] using norm_smoothGradToLp_eq hΩ (hφtest n)        _ = (eLpNorm (smoothGradField (φ n)) 2 μ).toReal := by              symm              rw [MeasureTheory.toReal_eLpNorm hgrad_memLp.aestronglyMeasurable]              simpa using                (MeasureTheory.lpNorm_eq_integral_norm_rpow_toReal                  (μ := μ) (f := smoothGradField (φ n)) (p := (2 : ENNReal))                  (by norm_num) (by simp) hgrad_memLp.aestronglyMeasurable)        _ = (eLpNorm (smoothGradNorm (φ n)) 2 μ).toReal := by              congr 1              calc                eLpNorm (smoothGradField (φ n)) 2 μ =                    eLpNorm (fun x => ‖smoothGradField (φ n) x‖) 2 μ := by                      symm                      exact eLpNorm_norm (μ := μ) (p := (2 : ENNReal)) (smoothGradField (φ n))                _ = eLpNorm (smoothGradNorm (φ n)) 2 μ := by                      simp [norm_smoothGradField_eq_smoothGradNorm]    rw [hfunEq, hgradEq]    convert hToReal using 1    rw [ENNReal.toReal_mul]  have hgrad_norm_tendsto :      Tendsto (fun n => ‖smoothGradToLp hΩ (hφtest n)‖) atTop (nhds 0) := by    have hnorm_tendsto :        Tendsto (fun n => ‖gradLpOfWitness (hφw n)‖) atTop (nhds 0) := by      simpa using ((continuous_norm.tendsto (0 : MeasureTheory.Lp E 2 μ)).comp hgradLp_zero_tendsto)    simpa [smoothGradToLp, hφw] using hnorm_tendsto  have hfun_norm_tendsto :      Tendsto (fun n => ‖smoothFunToLp hΩ (hφtest n)‖) atTop (nhds 0) := by    have hupper :        Tendsto (fun n => Cp.toReal * ‖smoothGradToLp hΩ (hφtest n)‖) atTop (nhds 0) := by      simpa using Tendsto.const_mul Cp.toReal hgrad_norm_tendsto    exact squeeze_zero (fun n => norm_nonneg _) hfun_bound hupper  have hfun_zero_tendsto :      Tendsto (fun n => smoothFunToLp hΩ (hφtest n)) atTop (nhds 0) := by    exact tendsto_zero_iff_norm_tendsto_zero.2 hfun_norm_tendsto  have hu_toLp_zero : hu_mem.1.toLp u = 0 := by    exact tendsto_nhds_unique hφ_fun_tendsto hfun_zero_tendsto  have htoLp_zero_ae : (hu_mem.1.toLp u : E → ℝ) =ᵐ[μ] (0 : E → ℝ) := by    let h0_mem : MemLp (0 : E → ℝ) 2 μ := MeasureTheory.MemLp.zero'    have h0_ae : (h0_mem.toLp (0 : E → ℝ) : E → ℝ) =ᵐ[μ] (0 : E → ℝ) := by      exact MemLp.coeFn_toLp h0_mem    rw [hu_toLp_zero]    simpa [h0_mem.toLp_zero] using h0_ae  calc    u =ᵐ[μ] hu_mem.1.toLp u := (MemLp.coeFn_toLp hu_mem.1).symm    _ =ᵐ[μ] (0 : E → ℝ) := htoLp_zero_ae