Log gradient bound of supersolution

theorem log_gradient_bound_of_supersolution    {Ω : Set E} (hΩ : IsOpen Ω)    (A : EllipticCoeff d Ω)    {u : E → ℝ}    (hu_pos : ∀ x ∈ Ω, 0 < u x)    (hsuper : IsSupersolution A u)    {φ : E → ℝ} (hφ : ContDiff ℝ (⊤ : ℕ∞) φ)    (hφ_cs : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ Ω)    (hw_u : MemW1pWitness 2 u Ω) :    ∫ x in Ω, φ x ^ 2 * ‖hw_u.weakGrad x‖ ^ 2 / (u x) ^ 2 ≤      4 * A.Λ / A.lam * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2 := by  -- The RHS is independent of ε, and for each ε > 0:  --   ∫ φ²|∇u|²/(u+ε)² ≤ 4Λ ∫ |∇φ|² (by log_gradient_bound_eps).  -- As ε ↘ 0, the LHS increases to ∫ φ²|∇u|²/u² (since u > 0 on Ω).  -- Apply monotone convergence to pass the bound to the limit.  suffices h : ∀ ε : ℝ, 0 < ε →      ∫ x in Ω, φ x ^ 2 * ‖hw_u.weakGrad x‖ ^ 2 / (u x + ε) ^ 2 ≤        4 * A.Λ / A.lam * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2 from by    let μ : Measure E := volume.restrict Ω    let εn : ℕ → ℝ := fun n => 1 / ((n : ℝ) + 1)    let g : ℕ → E → ℝ := fun n x =>      (φ x / (u x + εn n)) ^ 2 * ‖hw_u.weakGrad x‖ ^ 2    let g0 : E → ℝ := fun x =>      (φ x / u x) ^ 2 * ‖hw_u.weakGrad x‖ ^ 2    set R := 4 * A.Λ / A.lam * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2    obtain ⟨Cφ, hCφ⟩ := hφ_cs.exists_bound_of_continuous hφ.continuous    have hCφ_nonneg : 0 ≤ Cφ := le_trans (norm_nonneg _) (hCφ (0 : E))    have hεn_pos : ∀ n, 0 < εn n := by      intro n      dsimp [εn]      positivity    have hu_eps_aemeas : ∀ n, AEMeasurable (fun x => u x + εn n) μ := by      intro n      exact ((continuous_id.add continuous_const).comp_aestronglyMeasurable        hw_u.memLp.aestronglyMeasurable).aemeasurable    have hweight_sq_meas :        ∀ n, AEStronglyMeasurable (fun x => (φ x / (u x + εn n)) ^ 2) μ := by      intro n      exact ((hφ.continuous.aestronglyMeasurable.aemeasurable.div        (hu_eps_aemeas n)).pow_const 2).aestronglyMeasurable    have hweight_sq_bound :        ∀ n x, |(φ x / (u x + εn n)) ^ 2| ≤ Cφ ^ 2 / (εn n) ^ 2 := by      intro n x      by_cases hx : x ∈ Ω      · have hu_eps_pos : 0 < u x + εn n := by linarith [hu_pos x hx, hεn_pos n]        have hnum : |φ x| ≤ Cφ := (Real.norm_eq_abs (φ x)).symm ▸ hCφ x        have hnonneg : 0 ≤ Cφ / εn n := div_nonneg hCφ_nonneg (hεn_pos n).le        have hε_le : εn n ≤ u x + εn n := by linarith [hu_pos x hx]        have hbound : |φ x / (u x + εn n)| ≤ Cφ / εn n := by          rw [abs_div, abs_of_nonneg hu_eps_pos.le]          refine le_trans ?_ (div_le_div_of_nonneg_right hnum (hεn_pos n).le)          exact div_le_div_of_nonneg_left (abs_nonneg _) (hεn_pos n) hε_le        calc          |(φ x / (u x + εn n)) ^ 2| = |φ x / (u x + εn n)| ^ 2 := by rw [abs_pow]          _ ≤ (Cφ / εn n) ^ 2 := by              nlinarith [hbound, abs_nonneg (φ x / (u x + εn n)), hnonneg]          _ = Cφ ^ 2 / (εn n) ^ 2 := by ring      · have hφ0 : φ x = 0 := by          by_contra hφx          exact hx (hφ_sub (subset_tsupport φ (Function.mem_support.mpr hφx)))        have hnonneg : 0 ≤ Cφ ^ 2 / (εn n) ^ 2 := by          positivity        simpa [hφ0] using hnonneg    have hgrad_sq_meas : AEStronglyMeasurable (fun x => ‖hw_u.weakGrad x‖ ^ 2) μ := by      exact (hw_u.weakGrad_norm_memLp.aestronglyMeasurable.aemeasurable.pow_const 2).aestronglyMeasurable    have hg_meas : ∀ n, AEMeasurable (g n) μ := by      intro n      exact (hweight_sq_meas n).aemeasurable.mul hgrad_sq_meas.aemeasurable    have hg0_meas : AEStronglyMeasurable g0 μ := by      exact ((hφ.continuous.aestronglyMeasurable.aemeasurable.div        hw_u.memLp.aestronglyMeasurable.aemeasurable).pow_const 2).aestronglyMeasurable.mul hgrad_sq_meas    have hg_nonneg : ∀ n, 0 ≤ᵐ[μ] g n := by      intro n      exact Filter.Eventually.of_forall fun x => by        dsimp [g]        exact mul_nonneg (sq_nonneg _) (sq_nonneg _)    have hg0_nonneg : 0 ≤ᵐ[μ] g0 := by      exact Filter.Eventually.of_forall fun x => by        dsimp [g0]        exact mul_nonneg (sq_nonneg _) (sq_nonneg _)    have hg_int : ∀ n, Integrable (g n) μ := by      intro n      exact (hw_u.weakGrad_norm_memLp.integrable_sq).bdd_mul        (c := Cφ ^ 2 / (εn n) ^ 2) (hweight_sq_meas n)        (Filter.Eventually.of_forall (hweight_sq_bound n))    have hright_eq :        ∀ n,          ∫⁻ x, ENNReal.ofReal (g n x) ∂μ =            ENNReal.ofReal (∫ x, g n x ∂μ) := by      intro n      exact        (MeasureTheory.ofReal_integral_eq_lintegral_ofReal          (μ := μ) (f := g n) (hg_int n) (hg_nonneg n)).symm    have hfR : ∀ n, ∫ x, g n x ∂μ ≤ R := by      intro n      have hbound := h (εn n) (hεn_pos n)      change ∫ x in Ω, g n x ∂volume ≤ R      have hEq :          ∫ x in Ω, g n x ∂volume =            ∫ x in Ω, φ x ^ 2 * ‖hw_u.weakGrad x‖ ^ 2 / (u x + εn n) ^ 2 ∂volume := by        refine integral_congr_ae ?_        filter_upwards with x        dsimp [g]        rw [div_pow]        ring      rw [hEq]      exact hbound    have hFatou :        ∫⁻ x, ENNReal.ofReal (g0 x) ∂μ ≤          atTop.liminf (fun n => ∫⁻ x, ENNReal.ofReal (g n x) ∂μ) := by      have hmeas :          ∀ n, AEMeasurable (fun x => ENNReal.ofReal (g n x)) μ := by        intro n        exact (hg_meas n).ennreal_ofReal      have hleft := MeasureTheory.lintegral_liminf_le' (μ := μ) hmeas      have hlim :          (fun x =>            Filter.liminf (fun n => ENNReal.ofReal (g n x)) atTop) =ᵐ[μ]              (fun x => ENNReal.ofReal (g0 x)) := by        filter_upwards [ae_restrict_mem hΩ.measurableSet] with x hx        have hu_posx : 0 < u x := hu_pos x hx        have hden_tend : Tendsto (fun n => u x + εn n) atTop (nhds (u x)) := by          simpa [εn, one_div] using            (tendsto_one_div_add_atTop_nhds_zero_nat.const_add (u x))        have hquot_tend :            Tendsto (fun n => φ x / (u x + εn n)) atTop (nhds (φ x / u x)) := by          exact Tendsto.div tendsto_const_nhds hden_tend hu_posx.ne'        have hreal_tend : Tendsto (fun n => g n x) atTop (nhds (g0 x)) := by          exact ((continuous_pow 2).tendsto (φ x / u x)).comp hquot_tend |>.mul tendsto_const_nhds        have henn_tend :            Tendsto (fun n => ENNReal.ofReal (g n x)) atTop              (nhds (ENNReal.ofReal (g0 x))) := by          exact (ENNReal.continuous_ofReal.tendsto _).comp hreal_tend        exact henn_tend.liminf_eq      calc        ∫⁻ x, ENNReal.ofReal (g0 x) ∂μ            = ∫⁻ x, Filter.liminf (fun n => ENNReal.ofReal (g n x)) atTop ∂μ := by                exact lintegral_congr_ae hlim.symm        _ ≤ atTop.liminf (fun n => ∫⁻ x, ENNReal.ofReal (g n x) ∂μ) := hleft    have hliminf_le :        atTop.liminf (fun n => ∫⁻ x, ENNReal.ofReal (g n x) ∂μ) ≤ ENNReal.ofReal R := by      rw [Filter.liminf_congr (Eventually.of_forall hright_eq)]      refine Filter.liminf_le_of_frequently_le' (Frequently.of_forall fun n => ?_)      exact ENNReal.ofReal_le_ofReal (hfR n)    have hmain_enn : ∫⁻ x, ENNReal.ofReal (g0 x) ∂μ ≤ ENNReal.ofReal R := by      exact le_trans hFatou hliminf_le    have hR_nonneg : 0 ≤ R := by      dsimp [R]      refine mul_nonneg ?_ (integral_nonneg (fun x => by positivity))      · have hnum_nonneg : 0 ≤ 4 * A.Λ := by nlinarith [A.Λ_nonneg]        exact div_nonneg hnum_nonneg A.hlam.le    calc      ∫ x in Ω, φ x ^ 2 * ‖hw_u.weakGrad x‖ ^ 2 / (u x) ^ 2          = ∫ x, g0 x ∂μ := by              refine integral_congr_ae ?_              filter_upwards with x              dsimp [g0]              rw [div_pow]              ring      _ = ENNReal.toReal (∫⁻ x, ENNReal.ofReal (g0 x) ∂μ) := by            exact MeasureTheory.integral_eq_lintegral_of_nonneg_ae hg0_nonneg hg0_meas      _ ≤ ENNReal.toReal (ENNReal.ofReal R) := by            have hleft_ne_top : ∫⁻ x, ENNReal.ofReal (g0 x) ∂μ ≠ ∞ := by              exact ne_of_lt (lt_of_le_of_lt hmain_enn (by simp))            exact (ENNReal.toReal_le_toReal hleft_ne_top (by simp)).2 hmain_enn      _ = R := by rw [ENNReal.toReal_ofReal hR_nonneg]      _ = 4 * A.Λ / A.lam * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2 := by            rfl  intro ε hε  exact log_gradient_bound_eps hΩ A hu_pos hsuper hφ hφ_cs hφ_sub hw_u hε