Moser Reg Power Cutoff Witness norm sq le

lemma moserRegPowerCutoffWitness_norm_sq_le    {u η : E → ℝ} {s ε N p Cη : ℝ}    (hs : 0 < s) (hs1 : s ≤ 1) (hε : 0 < ε) (hN : 0 ≤ N)    (hu1 : MemW1pWitness 2 u (Metric.ball (0 : E) 1))    (hη : ContDiff ℝ (⊤ : ℕ∞) η)    (hη_bound : ∀ x, |η x| ≤ 1)    (hη_grad_bound : ∀ x, ‖fderiv ℝ η x‖ ≤ Cη)    (x : E) :    ‖(moserRegPowerCutoffWitness (d := d) (p := p)      hs hs1 hε hN hu1 hη hη_bound hη_grad_bound).weakGrad x‖ ^ 2 ≤      2 * (η x ^ 2 * (deriv (moserRegPow ε N p) (min (max (u x) 0) N)) ^ 2 *        ‖(moserClippedPosPartWitness (d := d) (u := u) hs hs1 hN hu1).weakGrad x‖ ^ 2) +      2 * (‖fderiv ℝ η x‖ ^ 2 *        (moserRegPow ε N p (min (max (u x) 0) N)) ^ 2) := by  -- The gradient identity is callable now that the /-! comment is fixed.  -- Componentwise: hwReg_i = η·α·clip_i + ∂ᵢη·β  -- where α = deriv(moserRegPow)(clip), β = moserRegPow(clip).  -- Also: hwComp_i = α · clip_i (from comp_smooth_bounded).  -- So (hwReg_i)² = (η·α·clip_i + ∂ᵢη·β)² ≤ 2(η·α·clip_i)² + 2(∂ᵢη·β)²  -- Summing: ‖hwReg‖² ≤ 2η²α²‖clip_grad‖² + 2β²‖∇η‖²  let hwClip := moserClippedPosPartWitness (d := d) (u := u) hs hs1 hN hu1  -- Componentwise bound  have hterm : ∀ i : Fin d,      (moserRegPowerCutoffWitness (d := d) (p := p)        hs hs1 hε hN hu1 hη hη_bound hη_grad_bound).weakGrad x i ^ 2 ≤      2 * (η x * deriv (moserRegPow ε N p) (min (max (u x) 0) N) *        hwClip.weakGrad x i) ^ 2 +      2 * ((fderiv ℝ η x) (EuclideanSpace.single i 1) *        moserRegPow ε N p (min (max (u x) 0) N)) ^ 2 := by    intro i    -- Use gradient identity + comp_smooth_bounded unfolding    have hgi := moserRegPowerCutoffWitness_grad (d := d) (p := p) hs hs1 hε hN hu1      hη hη_bound hη_grad_bound x i    have hcomp : (moserRegClippedPosPartWitness (d := d) (u := u) (p := p)        hs hs1 hε hN hu1).weakGrad x i =      deriv (moserRegPow ε N p) (min (max (u x) 0) N) * hwClip.weakGrad x i := by      set_option maxHeartbeats 400000 in      simp only [moserRegClippedPosPartWitness, MemW1pWitness.comp_smooth_bounded]      ring    rw [hgi, hcomp]    nlinarith [sq_nonneg (η x * (deriv (moserRegPow ε N p) (min (max (u x) 0) N) *      hwClip.weakGrad x i) -      (fderiv ℝ η x) (EuclideanSpace.single i 1) *      moserRegPow ε N p (min (max (u x) 0) N))]  -- Convert ‖·‖² to Σᵢ and back using EuclideanSpace.norm_eq  rw [EuclideanSpace.norm_eq (𝕜 := ℝ),    Real.sq_sqrt (Finset.sum_nonneg fun i _ => by positivity)]  simp_rw [Real.norm_eq_abs, sq_abs]  rw [EuclideanSpace.norm_eq (𝕜 := ℝ) (hwClip.weakGrad x),    Real.sq_sqrt (Finset.sum_nonneg fun i _ => by positivity)]  simp_rw [Real.norm_eq_abs, sq_abs]  -- Expand ‖fderiv ℝ η x‖² as sum  rw [show ‖fderiv ℝ η x‖ ^ 2 = ∑ i : Fin d,      ((fderiv ℝ η x) (EuclideanSpace.single i 1)) ^ 2 by    rw [← moser_norm_fderivVec_eq_norm_fderiv (d := d) (η := η) (x := x),      EuclideanSpace.norm_eq (𝕜 := ℝ),      Real.sq_sqrt (Finset.sum_nonneg fun i _ => by positivity)]    simp_rw [Real.norm_eq_abs, sq_abs, moserFderivVec_apply]]  -- Sum the componentwise bounds and factor  calc ∑ i, (moserRegPowerCutoffWitness (d := d) (p := p)          hs hs1 hε hN hu1 hη hη_bound hη_grad_bound).weakGrad x i ^ 2      ≤ ∑ i, (2 * (η x * deriv (moserRegPow ε N p) (min (max (u x) 0) N) *            hwClip.weakGrad x i) ^ 2 +          2 * ((fderiv ℝ η x) (EuclideanSpace.single i 1) *            moserRegPow ε N p (min (max (u x) 0) N)) ^ 2) :=        Finset.sum_le_sum fun i _ => hterm i    _ = 2 * (η x ^ 2 * deriv (moserRegPow ε N p) (min (max (u x) 0) N) ^ 2 *          ∑ i, hwClip.weakGrad x i ^ 2) +        2 * ((∑ i, ((fderiv ℝ η x) (EuclideanSpace.single i 1)) ^ 2) *          moserRegPow ε N p (min (max (u x) 0) N) ^ 2) := by        have : ∀ i : Fin d,            2 * (η x * deriv (moserRegPow ε N p) (min (max (u x) 0) N) *              hwClip.weakGrad x i) ^ 2 +            2 * ((fderiv ℝ η x) (EuclideanSpace.single i 1) *              moserRegPow ε N p (min (max (u x) 0) N)) ^ 2 =            2 * (η x ^ 2 * deriv (moserRegPow ε N p) (min (max (u x) 0) N) ^ 2 *              (hwClip.weakGrad x i ^ 2)) +            2 * (((fderiv ℝ η x) (EuclideanSpace.single i 1)) ^ 2 *              moserRegPow ε N p (min (max (u x) 0) N) ^ 2) := by          intro i; ring        simp_rw [this, Finset.sum_add_distrib, ← Finset.mul_sum]        simp [mul_comm, mul_left_comm, mul_assoc, ← Finset.mul_sum]