Divergence RHSOf Field bound

theorem divergenceRHSOfField_bound    {Ω : Set E} {F : E → E} (hF : MemLp F 2 (volume.restrict Ω))    {v : E → ℝ} (hv : MemW1pWitness 2 v Ω) :    |divergenceRHSOfField F hv| ≤      (∫ x, ‖F x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ)) *        (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ)) := by  let μ : Measure E := volume.restrict Ω  have hint_int := integrable_divergenceRHSIntegrandOfField hF hv  have hpointwise :      ∀ᵐ x ∂μ, ‖divergenceRHSIntegrandOfField F hv x‖ ≤ ‖F x‖ * ‖hv.weakGrad x‖ := by    filter_upwards with x    simpa [divergenceRHSIntegrandOfField] using abs_real_inner_le_norm (F x) (hv.weakGrad x)  have hnorm_le :      ∫ x, ‖divergenceRHSIntegrandOfField F hv x‖ ∂μ ≤        ∫ x, ‖F x‖ * ‖hv.weakGrad x‖ ∂μ := by    have hdom_int : Integrable (fun x => ‖F x‖ * ‖hv.weakGrad x‖) μ := by      simpa [mul_comm] using (hv.weakGrad_memLp.norm.integrable_mul hF.norm)    exact integral_mono_ae hint_int.norm hdom_int hpointwise  have hF_memLp : MemLp F (ENNReal.ofReal (2 : ℝ)) μ := by    simpa using hF  have hholder :      ∫ x, ‖F x‖ * ‖hv.weakGrad x‖ ∂μ ≤        (∫ x, ‖F x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) *          (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) := by    have hhv_memLp : MemLp hv.weakGrad (ENNReal.ofReal (2 : ℝ)) μ := by      simpa using hv.weakGrad_memLp    exact      integral_mul_norm_le_Lp_mul_Lq (μ := μ) (f := F) (g := hv.weakGrad)        Real.HolderConjugate.two_two hF_memLp hhv_memLp  simpa [divergenceRHSOfField, μ] using    (calc      |divergenceRHSOfField F hv| = ‖∫ x, divergenceRHSIntegrandOfField F hv x ∂μ‖ := by        simp [divergenceRHSOfField, μ]      _ ≤ ∫ x, ‖divergenceRHSIntegrandOfField F hv x‖ ∂μ :=        norm_integral_le_integral_norm _      _ ≤ ∫ x, ‖F x‖ * ‖hv.weakGrad x‖ ∂μ := hnorm_le      _ ≤        (∫ x, ‖F x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) *          (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) := hholder)