Bilin Form bound

theorem bilinForm_bound    {Ω : Set E} {u v : E → ℝ}    (A : EllipticCoeff d Ω)    (hu : MemW1pWitness 2 u Ω) (hv : MemW1pWitness 2 v Ω) :    |bilinFormOfCoeff A hu hv| ≤      A.Λ * (∫ x, ‖hu.weakGrad 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_bilinFormIntegrandOfCoeff A hu hv  have hdom_int :      Integrable (fun x => A.Λ * (‖hu.weakGrad x‖ * ‖hv.weakGrad x‖)) μ := by    rw [← memLp_one_iff_integrable]    have hprod_memLp :        MemLp (fun x => ‖hu.weakGrad x‖ * ‖hv.weakGrad x‖) 1 μ := by      simpa using (hv.weakGrad_memLp.norm.mul hu.weakGrad_memLp.norm)    exact hprod_memLp.const_mul A.Λ  have hpointwise :      ∀ᵐ x ∂μ, ‖bilinFormIntegrandOfCoeff A hu hv x‖ ≤        A.Λ * (‖hu.weakGrad x‖ * ‖hv.weakGrad x‖) := by    filter_upwards [A.mixed_bound] with x hx    simpa [bilinFormIntegrandOfCoeff, real_inner_comm, mul_assoc, mul_comm, mul_left_comm] using      hx (hu.weakGrad x) (hv.weakGrad x)  have hnorm_le :      ∫ x, ‖bilinFormIntegrandOfCoeff A hu hv x‖ ∂μ ≤        ∫ x, A.Λ * (‖hu.weakGrad x‖ * ‖hv.weakGrad x‖) ∂μ := by    exact integral_mono_ae hint_int.norm hdom_int hpointwise  have hholder :      ∫ x, ‖hu.weakGrad x‖ * ‖hv.weakGrad x‖ ∂μ ≤        (∫ x, ‖hu.weakGrad x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) *          (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) := by    have hhu_memLp : MemLp hu.weakGrad (ENNReal.ofReal (2 : ℝ)) μ := by      simpa using hu.weakGrad_memLp    have hhv_memLp : MemLp hv.weakGrad (ENNReal.ofReal (2 : ℝ)) μ := by      simpa using hv.weakGrad_memLp    exact      integral_mul_norm_le_Lp_mul_Lq (μ := μ) (f := hu.weakGrad) (g := hv.weakGrad)        Real.HolderConjugate.two_two hhu_memLp hhv_memLp  simpa [μ, mul_assoc] using    (calc      |bilinFormOfCoeff A hu hv| = ‖∫ x, bilinFormIntegrandOfCoeff A hu hv x ∂μ‖ := by        simp [bilinFormOfCoeff, μ]      _ ≤ ∫ x, ‖bilinFormIntegrandOfCoeff A hu hv x‖ ∂μ :=        norm_integral_le_integral_norm _      _ ≤ ∫ x, A.Λ * (‖hu.weakGrad x‖ * ‖hv.weakGrad x‖) ∂μ := hnorm_le      _ = A.Λ * ∫ x, ‖hu.weakGrad x‖ * ‖hv.weakGrad x‖ ∂μ := by        rw [integral_const_mul]      _ ≤ A.Λ *          ((∫ x, ‖hu.weakGrad x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) *            (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ))) := by        exact mul_le_mul_of_nonneg_left hholder A.Λ_nonneg      _ = A.Λ * (∫ x, ‖hu.weakGrad x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) *          (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) ∂μ) ^ (1 / (2 : ℝ)) := by        ring)