Weak Solution stability

theorem weakSolution_stability    {Ω : Set E}    (A : EllipticCoeff d Ω)    {u : E → ℝ}    (hu0 : MemH01 u Ω)    (hwu : MemW1pWitness 2 u Ω)    {rhs : (E → ℝ) → ℝ}    {C_F : ℝ} (hCF : 0 ≤ C_F)    (hF : ∀ v : E → ℝ, MemH01 v Ω →      ∀ hwv : MemW1pWitness 2 v Ω,      |rhs v| ≤ C_F *        (∫ x, ‖hwv.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ)))    (h_ws : bilinFormOfCoeff A hwu hwu = rhs u) :    (∫ x, ‖hwu.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ)) ≤    A.lam⁻¹ * C_F := by  let μ : Measure E := volume.restrict Ω  let J : ℝ := ∫ x, ‖hwu.weakGrad x‖ ^ (2 : ℕ) ∂μ  have hJ_nonneg : 0 ≤ J := by    dsimp [J]    refine integral_nonneg ?_    intro x    positivity  have hnorm_eq :      ‖gradLpOfWitness hwu‖ = Real.sqrt J := by    calc      ‖gradLpOfWitness hwu‖          = (∫ x, ‖hwu.weakGrad x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) := by              simpa [μ] using norm_gradLpOfWitness_eq hwu      _ = J ^ (1 / (2 : ℝ)) := by            congr 1            dsimp [J]            apply integral_congr_ae            filter_upwards with x            exact Real.rpow_natCast ‖hwu.weakGrad x‖ 2      _ = Real.sqrt J := by            rw [Real.sqrt_eq_rpow]  have hnorm_sq :      ‖gradLpOfWitness hwu‖ ^ (2 : ℕ) = J := by    calc      ‖gradLpOfWitness hwu‖ ^ (2 : ℕ) = (Real.sqrt J) ^ (2 : ℕ) := by rw [hnorm_eq]      _ = J := by simpa [pow_two] using Real.sq_sqrt hJ_nonneg  have hcoercive :      A.lam * ‖gradLpOfWitness hwu‖ ^ (2 : ℕ) ≤ bilinFormOfCoeff A hwu hwu := by    calc      A.lam * ‖gradLpOfWitness hwu‖ ^ (2 : ℕ) = A.lam * J := by rw [hnorm_sq]      _ = A.lam * ∫ x, ‖hwu.weakGrad x‖ ^ (2 : ℕ) ∂μ := by rfl      _ ≤ bilinFormOfCoeff A hwu hwu := by            simpa [μ] using bilinForm_coercive A hwu  have h_rhs_bound : |rhs u| ≤ C_F * ‖gradLpOfWitness hwu‖ := by    calc      |rhs u| ≤ C_F * (∫ x, ‖hwu.weakGrad x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) := hF u hu0 hwu      _ = C_F * ‖gradLpOfWitness hwu‖ := by rw [norm_gradLpOfWitness_eq hwu]  have hbilin_nonneg : 0 ≤ bilinFormOfCoeff A hwu hwu := by    exact le_trans (mul_nonneg A.lam_nonneg (sq_nonneg ‖gradLpOfWitness hwu‖)) hcoercive  have hrhs_nonneg : 0 ≤ rhs u := by    simpa [h_ws] using hbilin_nonneg  have hmain :      A.lam * ‖gradLpOfWitness hwu‖ ^ (2 : ℕ) ≤ C_F * ‖gradLpOfWitness hwu‖ := by    calc      A.lam * ‖gradLpOfWitness hwu‖ ^ (2 : ℕ) ≤ bilinFormOfCoeff A hwu hwu := hcoercive      _ = rhs u := h_ws      _ = |rhs u| := by symm; exact abs_of_nonneg hrhs_nonneg      _ ≤ C_F * ‖gradLpOfWitness hwu‖ := h_rhs_bound  have hlin :      A.lam * ‖gradLpOfWitness hwu‖ ≤ C_F := by    have hmain' :        A.lam * ‖gradLpOfWitness hwu‖ ^ 2 ≤ C_F * ‖gradLpOfWitness hwu‖ := by      simpa [pow_two] using hmain    nlinarith [hmain', A.hlam, norm_nonneg (gradLpOfWitness hwu)]  have hdiv :      ‖gradLpOfWitness hwu‖ ≤ C_F / A.lam := by    have hlin' : ‖gradLpOfWitness hwu‖ * A.lam ≤ C_F := by      simpa [mul_comm] using hlin    exact (le_div_iff₀ A.hlam).2 hlin'  simpa [norm_gradLpOfWitness_eq hwu, div_eq_mul_inv, mul_comm] using hdiv