Log gradient bound eps

theorem log_gradient_bound_eps    {Ω : 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 Ω)    {ε : ℝ} (hε : 0 < ε) :    ∫ x in Ω, φ x ^ 2 * ‖hw_u.weakGrad x‖ ^ 2 / (u x + ε) ^ 2 ≤      4 * A.Λ / A.lam * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2 := by  -- Define the key integrals.  set LHS := ∫ x in Ω, φ x ^ 2 * ‖hw_u.weakGrad x‖ ^ 2 / (u x + ε) ^ 2  -- Q := ∫ φ²/(u+ε)² ⟨∇u, A∇u⟩ (A-quadratic form weighted by φ²/(u+ε)²)  set Q := ∫ x in Ω, φ x ^ 2 / (u x + ε) ^ 2 *    @inner ℝ E _ (hw_u.weakGrad x) (matMulE (A.a x) (hw_u.weakGrad x))  -- X := ∫ φ/(u+ε) ⟨∇φ, A∇u⟩ (mixed A-form)  set gradφ : E → E := fun x => WithLp.toLp 2    (fun i => (fderiv ℝ φ x) (EuclideanSpace.single i 1))  set X := ∫ x in Ω, φ x / (u x + ε) *    @inner ℝ E _ (gradφ x) (matMulE (A.a x) (hw_u.weakGrad x))  -- Step (b): Q ≤ 2X (from supersolution with ψ_ε = φ²/(u+ε))  have hQ_le_2X : Q ≤ 2 * X :=    supersolution_energy_identity_eps hΩ A hu_pos hsuper hw_u hφ hφ_cs hφ_sub hε  -- Q ≥ 0 (by coercivity: ⟨ξ, Aξ⟩ ≥ λ‖ξ‖² ≥ 0)  have hQ_nonneg : 0 ≤ Q := by    apply integral_nonneg_of_ae    filter_upwards [A.ae_coercive_nonneg] with x hx    exact mul_nonneg (div_nonneg (sq_nonneg _) (sq_nonneg _)) (hx (hw_u.weakGrad x))  have hu_eps_aemeas : AEMeasurable (fun x => u x + ε) (volume.restrict Ω) := by    exact ((continuous_id.add continuous_const).comp_aestronglyMeasurable      hw_u.memLp.aestronglyMeasurable).aemeasurable  have hweight_aemeas : AEMeasurable (fun x => φ x / (u x + ε)) (volume.restrict Ω) := by    exact (hφ.continuous.aestronglyMeasurable.aemeasurable.div hu_eps_aemeas)  have hweight_sq_meas :      AEStronglyMeasurable (fun x => (φ x / (u x + ε)) ^ 2) (volume.restrict Ω) := by    exact (hweight_aemeas.pow_const 2).aestronglyMeasurable  obtain ⟨Cφ, hCφ⟩ := hφ_cs.exists_bound_of_continuous hφ.continuous  have hCφ_nonneg : 0 ≤ Cφ := le_trans (norm_nonneg _) (hCφ (0 : E))  have hweight_bound : ∀ x, |φ x / (u x + ε)| ≤ Cφ / ε := by    intro x    by_cases hx : x ∈ Ω    · have hu_eps_pos : 0 < u x + ε := by linarith [hu_pos x hx, hε]      have hnum : |φ x| ≤ Cφ := (Real.norm_eq_abs (φ x)).symm ▸ hCφ x      rw [abs_div, abs_of_nonneg hu_eps_pos.le]      have hε_le : ε ≤ u x + ε := by linarith [hu_pos x hx]      have hgoal : |φ x| / (u x + ε) ≤ Cφ / ε := by        refine le_trans ?_ (div_le_div_of_nonneg_right hnum hε.le)        exact div_le_div_of_nonneg_left (abs_nonneg _) hε hε_le      simpa [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using hgoal    · have hφ0 : φ x = 0 := by        by_contra h        exact hx (hφ_sub (subset_tsupport φ (Function.mem_support.mpr h)))      have hnonneg : 0 ≤ Cφ / ε := div_nonneg hCφ_nonneg hε.le      simpa [hφ0] using hnonneg  have hweight_sq_bound : ∀ x, |(φ x / (u x + ε)) ^ 2| ≤ Cφ ^ 2 / ε ^ 2 := by    intro x    have hx := hweight_bound x    have hnonneg : 0 ≤ Cφ / ε := div_nonneg hCφ_nonneg hε.le    calc      |(φ x / (u x + ε)) ^ 2| = |φ x / (u x + ε)| ^ 2 := by rw [abs_pow]      _ ≤ (Cφ / ε) ^ 2 := by nlinarith [hx, abs_nonneg (φ x / (u x + ε)), hnonneg]      _ = Cφ ^ 2 / ε ^ 2 := by ring  have hQ_int_weight :      Integrable (fun x => (φ x / (u x + ε)) ^ 2 *        bilinFormIntegrandOfCoeff A hw_u hw_u x) (volume.restrict Ω) := by    exact integrable_bounded_mul_bilinFormIntegrand A hw_u hweight_sq_meas hweight_sq_bound  have hQ_int :      Integrable (fun x => φ x ^ 2 / (u x + ε) ^ 2 *        bilinFormIntegrandOfCoeff A hw_u hw_u x) (volume.restrict Ω) := by    convert hQ_int_weight using 1    ext x    rw [bilinFormIntegrandOfCoeff, real_inner_comm]    rw [div_pow]  have hQ_eq :      ∫ x in Ω, φ x ^ 2 / (u x + ε) ^ 2 * bilinFormIntegrandOfCoeff A hw_u hw_u x = Q := by    change ∫ x in Ω, φ x ^ 2 / (u x + ε) ^ 2 * bilinFormIntegrandOfCoeff A hw_u hw_u x =      ∫ x in Ω, φ x ^ 2 / (u x + ε) ^ 2 *        @inner ℝ E _ (hw_u.weakGrad x) (matMulE (A.a x) (hw_u.weakGrad x))    refine integral_congr_ae ?_    filter_upwards with x    rw [bilinFormIntegrandOfCoeff, real_inner_comm]  -- Coercivity: λ · LHS ≤ Q (pointwise ⟨ξ, Aξ⟩ ≥ λ‖ξ‖², integrate)  have hLHS_le : A.lam * LHS ≤ Q := by    let leftInt : E → ℝ := fun x =>      A.lam * ((φ x / (u x + ε)) ^ 2 * ‖hw_u.weakGrad x‖ ^ 2)    have hleft_aemeas : AEMeasurable leftInt (volume.restrict Ω) := by      exact (((hweight_aemeas.pow_const 2).mul        (hw_u.weakGrad_norm_memLp.aestronglyMeasurable.aemeasurable.pow_const 2)).const_mul A.lam)    have hleft_meas : AEStronglyMeasurable leftInt (volume.restrict Ω) :=      hleft_aemeas.aestronglyMeasurable    have hleft_le_q :        ∀ᵐ x ∂(volume.restrict Ω),          leftInt x ≤ φ x ^ 2 / (u x + ε) ^ 2 *            bilinFormIntegrandOfCoeff A hw_u hw_u x := by      filter_upwards [A.coercive] with x hx      have hnn : 0 ≤ (φ x / (u x + ε)) ^ 2 := sq_nonneg _      calc        leftInt x            = (φ x / (u x + ε)) ^ 2 * (A.lam * ‖hw_u.weakGrad x‖ ^ 2) := by                dsimp [leftInt]                ring        _ ≤ (φ x / (u x + ε)) ^ 2 *              @inner ℝ E _ (hw_u.weakGrad x) (matMulE (A.a x) (hw_u.weakGrad x)) :=            mul_le_mul_of_nonneg_left (hx (hw_u.weakGrad x)) hnn        _ = φ x ^ 2 / (u x + ε) ^ 2 *              bilinFormIntegrandOfCoeff A hw_u hw_u x := by            rw [bilinFormIntegrandOfCoeff, real_inner_comm]            rw [div_pow]    have hleft_int : Integrable leftInt (volume.restrict Ω) := by      refine Integrable.mono' hQ_int hleft_meas ?_      filter_upwards [hleft_le_q] with x hx      have hleft_nonneg : 0 ≤ leftInt x := by        dsimp [leftInt]        exact mul_nonneg A.lam_nonneg (mul_nonneg (sq_nonneg _) (sq_nonneg _))      rw [Real.norm_of_nonneg hleft_nonneg]      exact hx    calc A.lam * LHS        = ∫ x in Ω, A.lam * (φ x ^ 2 * ‖hw_u.weakGrad x‖ ^ 2 / (u x + ε) ^ 2) := by          rw [integral_const_mul]      _ = ∫ x in Ω, leftInt x := by          refine integral_congr_ae ?_          filter_upwards with x          dsimp [leftInt]          rw [div_pow]          ring      _ ≤ ∫ x in Ω, φ x ^ 2 / (u x + ε) ^ 2 * bilinFormIntegrandOfCoeff A hw_u hw_u x := by          exact integral_mono_ae hleft_int hQ_int hleft_le_q      _ = Q := hQ_eq  have hφ_test : IsSmoothTestOn Ω φ := ⟨hφ, hφ_cs, hφ_sub⟩  let hw_φ : MemW1pWitness 2 φ Ω := smoothTestWitness hΩ hφ_test  have hX_sq_le :      X ^ 2 ≤ Q * (A.Λ * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2) := by    have hcs :=      bilinForm_weighted_cauchySchwarz        (A := A) (hu := hw_u) (hv := hw_φ)        (f := fun x => φ x / (u x + ε))        hweight_aemeas.aestronglyMeasurable hQ_int_weight    have hX_eq :        ∫ x in Ω, φ x / (u x + ε) *          bilinFormIntegrandOfCoeff A hw_u hw_φ x = X := by      change ∫ x in Ω, φ x / (u x + ε) * bilinFormIntegrandOfCoeff A hw_u hw_φ x =        ∫ x in Ω, φ x / (u x + ε) *          @inner ℝ E _ (gradφ x) (matMulE (A.a x) (hw_u.weakGrad x))      refine integral_congr_ae ?_      filter_upwards with x      rw [bilinFormIntegrandOfCoeff, real_inner_comm]      simp [gradφ, hw_φ, smoothTestWitness, smoothGradField]    have hgrad_sq_eq :        ∀ x, ‖hw_φ.weakGrad x‖ ^ (2 : ℕ) = ‖fderiv ℝ φ x‖ ^ 2 := by      intro x      have hnorm : ‖hw_φ.weakGrad x‖ = ‖fderiv ℝ φ x‖ := by        simp [hw_φ, smoothTestWitness, smoothGradField, smoothGradNorm,          norm_fderiv_eq_smoothGradNorm]      rw [hnorm]    have hP_eq :        ∫ x in Ω, ‖hw_φ.weakGrad x‖ ^ (2 : ℕ) =          ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2 := by      exact integral_congr_ae (Filter.Eventually.of_forall hgrad_sq_eq)    calc      X ^ 2 = (∫ x in Ω, φ x / (u x + ε) *          bilinFormIntegrandOfCoeff A hw_u hw_φ x) ^ 2 := by            rw [hX_eq.symm]      _ ≤ (∫ x in Ω, (φ x / (u x + ε)) ^ 2 *            bilinFormIntegrandOfCoeff A hw_u hw_u x) *          (A.Λ * ∫ x in Ω, ‖hw_φ.weakGrad x‖ ^ (2 : ℕ)) := hcs      _ = Q * (A.Λ * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2) := by          rw [show ∫ x in Ω, (φ x / (u x + ε)) ^ 2 * bilinFormIntegrandOfCoeff A hw_u hw_u x =              ∫ x in Ω, φ x ^ 2 / (u x + ε) ^ 2 * bilinFormIntegrandOfCoeff A hw_u hw_u x by                refine integral_congr_ae ?_                filter_upwards with x                rw [div_pow],            hQ_eq, hP_eq]  have hR_nonneg : 0 ≤ A.Λ * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2 := by    refine mul_nonneg A.Λ_nonneg ?_    exact integral_nonneg (fun x => by positivity)  have hlamLHS_le :      A.lam * LHS ≤ 4 * (A.Λ * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2) := by    exact      log_gradient_algebraic_conclusion        (Q := Q) (X := X) (P := A.Λ * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2)        (LHS := A.lam * LHS) (RHS := A.Λ * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2)        hQ_nonneg hR_nonneg hQ_le_2X hX_sq_le hLHS_le le_rfl  calc    LHS ≤ (4 * (A.Λ * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2)) / A.lam := by      rw [le_div_iff₀ A.hlam]      simpa [mul_comm] using hlamLHS_le    _ = 4 * A.Λ / A.lam * ∫ x in Ω, ‖fderiv ℝ φ x‖ ^ 2 := by ring