Bilin Form weighted cauchy Schwarz

theorem bilinForm_weighted_cauchySchwarz    {Ω : Set E}    {u v : E → ℝ} {f : E → ℝ}    (A : EllipticCoeff d Ω)    (hu : MemW1pWitness 2 u Ω) (hv : MemW1pWitness 2 v Ω)    (hf : AEStronglyMeasurable f (volume.restrict Ω))    (hf_sq_int : Integrable (fun x => f x ^ 2 *        bilinFormIntegrandOfCoeff A hu hu x) (volume.restrict Ω)) :    (∫ x in Ω, f x * bilinFormIntegrandOfCoeff A hu hv x ∂volume) ^ 2 ≤      (∫ x in Ω, f x ^ 2 * bilinFormIntegrandOfCoeff A hu hu x ∂volume) *        (A.Λ * ∫ x in Ω, ‖hv.weakGrad x‖ ^ (2 : ℕ) ∂volume) := by  let μ : Measure E := volume.restrict Ω  -- Non-integrable case: integral = 0, so 0² = 0 ≤ RHS  by_cases hint : Integrable (fun x => f x * bilinFormIntegrandOfCoeff A hu hv x) μ  · -- Integrable case: use pointwise bound + Hölder    have hpw_abs : ∀ᵐ x ∂μ, ‖f x * bilinFormIntegrandOfCoeff A hu hv x‖ ≤        (|f x| * ‖matMulE (A.a x) (hu.weakGrad x)‖) * ‖hv.weakGrad x‖ := by      filter_upwards with x      rw [Real.norm_eq_abs, abs_mul, bilinFormIntegrandOfCoeff]      calc |f x| * |⟪matMulE (A.a x) (hu.weakGrad x), hv.weakGrad x⟫_ℝ|          ≤ |f x| * (‖matMulE (A.a x) (hu.weakGrad x)‖ * ‖hv.weakGrad x‖) :=            mul_le_mul_of_nonneg_left (abs_real_inner_le_norm _ _) (abs_nonneg _)        _ = (|f x| * ‖matMulE (A.a x) (hu.weakGrad x)‖) * ‖hv.weakGrad x‖ := by ring    have hdom : ∀ᵐ x ∂μ, f x ^ 2 * ‖matMulE (A.a x) (hu.weakGrad x)‖ ^ 2 ≤        A.Λ * (f x ^ 2 * bilinFormIntegrandOfCoeff A hu hu x) := by      filter_upwards [A.mulVec_sq_le] with x hx      have hmvs := hx (hu.weakGrad x)      calc f x ^ 2 * ‖matMulE (A.a x) (hu.weakGrad x)‖ ^ 2          ≤ f x ^ 2 * (A.Λ * ⟪hu.weakGrad x, matMulE (A.a x) (hu.weakGrad x)⟫_ℝ) :=            mul_le_mul_of_nonneg_left hmvs (sq_nonneg _)        _ = A.Λ * (f x ^ 2 * ⟪hu.weakGrad x, matMulE (A.a x) (hu.weakGrad x)⟫_ℝ) := by ring        _ = A.Λ * (f x ^ 2 * bilinFormIntegrandOfCoeff A hu hu x) := by            rw [bilinFormIntegrandOfCoeff, real_inner_comm]    have hg_meas : AEStronglyMeasurable (fun x => |f x| * ‖matMulE (A.a x) (hu.weakGrad x)‖) μ :=      hf.norm.mul (aestronglyMeasurable_norm_matMulE_weakGrad A hu)    have hfsq_normAu_int : Integrable (fun x =>        f x ^ 2 * ‖matMulE (A.a x) (hu.weakGrad x)‖ ^ 2) μ := by      refine Integrable.mono' (hf_sq_int.const_mul A.Λ) ?_ ?_      · exact (hg_meas.mul hg_meas).congr (ae_of_all _ (fun x => by          simp only [Pi.mul_apply]; rw [← sq_abs (f x)]; ring))      · filter_upwards [hdom] with x hx        rw [Real.norm_of_nonneg (mul_nonneg (sq_nonneg _) (sq_nonneg _))]        exact hx    -- g² = f² * ‖A∇u‖² is integrable, so g ∈ L²    have hg_memLp : MemLp (fun x => |f x| * ‖matMulE (A.a x) (hu.weakGrad x)‖)        (ENNReal.ofReal 2) μ := by      rw [show (ENNReal.ofReal (2 : ℝ)) = (2 : ℕ∞) from by norm_num]      exact memLp_abs_mul_norm_matMulE A hu hf hfsq_normAu_int    -- h(x) = ‖∇v(x)‖    have hh_memLp : MemLp (fun x => ‖hv.weakGrad x‖)        (ENNReal.ofReal 2) μ := by      rw [show (ENNReal.ofReal (2 : ℝ)) = (2 : ℕ∞) from by norm_num]      exact hv.weakGrad_memLp.norm    have hholder :=      integral_mul_norm_le_Lp_mul_Lq (μ := μ)        (f := fun x => |f x| * ‖matMulE (A.a x) (hu.weakGrad x)‖)        (g := fun x => ‖hv.weakGrad x‖)        Real.HolderConjugate.two_two hg_memLp hh_memLp    simp only [Real.norm_of_nonneg (mul_nonneg (abs_nonneg _) (norm_nonneg _)),      Real.norm_of_nonneg (norm_nonneg _)] at hholder    -- |∫ f*bilin| ≤ ∫ |f*bilin| ≤ ∫ g*h ≤ (∫ g²)^(1/2) * (∫ h²)^(1/2)    -- Need: g*h integrable for integral_mono_ae    have hgh_int : Integrable (fun x =>        (|f x| * ‖matMulE (A.a x) (hu.weakGrad x)‖) * ‖hv.weakGrad x‖) μ := by      have hh2_int : Integrable (fun x => ‖hv.weakGrad x‖ ^ (2 : ℕ)) μ := by        have := (integrable_norm_rpow_iff          hv.weakGrad_memLp.aestronglyMeasurable.norm two_ne_zero ENNReal.ofNat_ne_top).mpr          hv.weakGrad_memLp.norm        convert this using 1; ext x        rw [Real.norm_of_nonneg (norm_nonneg _)]        have h2 : ENNReal.toReal 2 = (2 : ℝ) := by norm_num        rw [h2, show (2 : ℝ) = ((2 : ℕ) : ℝ) from by norm_num, Real.rpow_natCast]      refine Integrable.mono'        ((hfsq_normAu_int.add hh2_int).div_const 2)        (hg_meas.mul hv.weakGrad_memLp.aestronglyMeasurable.norm)        (ae_of_all _ (fun x => ?_))      rw [Real.norm_of_nonneg (mul_nonneg (mul_nonneg (abs_nonneg _) (norm_nonneg _))        (norm_nonneg _))]      simp only [Pi.add_apply]      have hg := mul_nonneg (abs_nonneg (f x)) (norm_nonneg (matMulE (A.a x) (hu.weakGrad x)))      have hh := norm_nonneg (hv.weakGrad x)      nlinarith [sq_nonneg (|f x| * ‖matMulE (A.a x) (hu.weakGrad x)‖ - ‖hv.weakGrad x‖),        sq_abs (f x), mul_self_nonneg (‖matMulE (A.a x) (hu.weakGrad x)‖)]    have habs_le : |∫ x, f x * bilinFormIntegrandOfCoeff A hu hv x ∂μ| ≤        ∫ x, (|f x| * ‖matMulE (A.a x) (hu.weakGrad x)‖) * ‖hv.weakGrad x‖ ∂μ := by      calc |∫ x, f x * bilinFormIntegrandOfCoeff A hu hv x ∂μ|          = ‖∫ x, f x * bilinFormIntegrandOfCoeff A hu hv x ∂μ‖ := (Real.norm_eq_abs _).symm        _ ≤ ∫ x, ‖f x * bilinFormIntegrandOfCoeff A hu hv x‖ ∂μ :=            norm_integral_le_integral_norm _        _ ≤ _ := integral_mono_ae hint.norm hgh_int hpw_abs    have hle_rpow : |∫ x, f x * bilinFormIntegrandOfCoeff A hu hv x ∂μ| ≤        (∫ x, (|f x| * ‖matMulE (A.a x) (hu.weakGrad x)‖) ^ (2 : ℝ) ∂μ) ^ ((1 : ℝ) / 2) *        (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) ∂μ) ^ ((1 : ℝ) / 2) :=      le_trans habs_le hholder    have hsq : (∫ x, f x * bilinFormIntegrandOfCoeff A hu hv x ∂μ) ^ (2 : ℕ) ≤        (∫ x, (|f x| * ‖matMulE (A.a x) (hu.weakGrad x)‖) ^ (2 : ℝ) ∂μ) *        (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) ∂μ) := by      have := sq_le_of_le_rpow_half_mul        (integral_nonneg (fun x => by positivity))        (integral_nonneg (fun x => by positivity))        (abs_nonneg _) hle_rpow      rwa [sq_abs] at this    have hrpow_g : ∀ x, (|f x| * ‖matMulE (A.a x) (hu.weakGrad x)‖) ^ (2 : ℝ) =        f x ^ 2 * ‖matMulE (A.a x) (hu.weakGrad x)‖ ^ 2 := by      intro x      rw [Real.mul_rpow (abs_nonneg _) (norm_nonneg _)]      rw [show (2 : ℝ) = ((2 : ℕ) : ℝ) from by norm_num]      rw [Real.rpow_natCast, Real.rpow_natCast, sq_abs]    have hrpow_h : ∀ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) = (‖hv.weakGrad x‖ ^ (2 : ℕ) : ℝ) := by      intro x      rw [show (2 : ℝ) = ((2 : ℕ) : ℝ) from by norm_num, Real.rpow_natCast]    simp_rw [hrpow_g, hrpow_h] at hsq    have hint_dom : ∫ x, f x ^ 2 * ‖matMulE (A.a x) (hu.weakGrad x)‖ ^ 2 ∂μ ≤        A.Λ * ∫ x, f x ^ 2 * bilinFormIntegrandOfCoeff A hu hu x ∂μ := by      calc ∫ x, f x ^ 2 * ‖matMulE (A.a x) (hu.weakGrad x)‖ ^ 2 ∂μ          ≤ ∫ x, A.Λ * (f x ^ 2 * bilinFormIntegrandOfCoeff A hu hu x) ∂μ :=            integral_mono_ae hfsq_normAu_int (hf_sq_int.const_mul A.Λ) hdom        _ = A.Λ * ∫ x, f x ^ 2 * bilinFormIntegrandOfCoeff A hu hu x ∂μ :=            integral_const_mul _ _    -- Final assembly    calc (∫ x, f x * bilinFormIntegrandOfCoeff A hu hv x ∂μ) ^ 2        ≤ (∫ x, f x ^ 2 * ‖matMulE (A.a x) (hu.weakGrad x)‖ ^ 2 ∂μ) *          (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℕ) ∂μ) := hsq      _ ≤ (A.Λ * ∫ x, f x ^ 2 * bilinFormIntegrandOfCoeff A hu hu x ∂μ) *          (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℕ) ∂μ) :=          mul_le_mul_of_nonneg_right hint_dom (integral_nonneg (fun x => by positivity))      _ = (∫ x, f x ^ 2 * bilinFormIntegrandOfCoeff A hu hu x ∂μ) *          (A.Λ * ∫ x, ‖hv.weakGrad x‖ ^ (2 : ℕ) ∂μ) := by ring  · -- Non-integrable case    have hlhs : ∫ x in Ω, f x * bilinFormIntegrandOfCoeff A hu hv x = 0 :=      integral_undef hint    rw [hlhs]    simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]    exact mul_nonneg      (integral_nonneg_of_ae (by        filter_upwards [A.coercive] with x hx        have hbilin_nonneg : 0 ≤ bilinFormIntegrandOfCoeff A hu hu x := by          simp only [bilinFormIntegrandOfCoeff]          rw [real_inner_comm]          exact le_trans (mul_nonneg A.lam_nonneg (sq_nonneg _)) (hx (hu.weakGrad x))        exact mul_nonneg (sq_nonneg _) hbilin_nonneg))      (mul_nonneg A.Λ_nonneg (integral_nonneg (fun x => by positivity)))