eLpNorm_czOperator_sq

lemma eLpNorm_czOperator_sq {g : ℝ → ℂ} {r : ℝ} (hr : r ∈ Ioo 0 1) (hg : MemLp g ∞ volume) :    (eLpNorm (czOperator K r g) 2) ^ 2 ≤ 2 ^ 18 * (eLpNorm g 2) ^ 2 := by  have A : (volume : Measure ℝ) =      Measure.sum (fun (n : ℤ) ↦ volume.restrict (Ioc (n : ℝ) (n + 1))) := by    rw [← restrict_iUnion (Set.pairwise_disjoint_Ioc_intCast _) (fun n ↦ measurableSet_Ioc),      iUnion_Ioc_intCast, restrict_univ]  /- There is a weird calc bug here: if one omits the implicit argument `volume` from the first  or the last line, `calc` loops forever... -/  calc  (eLpNorm (czOperator K r g) 2 volume) ^ 2  _ = ∫⁻ x, ‖czOperator K r g x‖ₑ ^ 2 := by rw [sq_eLpNorm_two]  _ = ∑' n : ℤ, ∫⁻ x in Ioc (n : ℝ) (n + 1), ‖czOperator K r g x‖ₑ ^ 2 := by    conv_lhs => rw [A, lintegral_sum_measure]  _ = ∑' n : ℤ, (eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc n (n + 1)))) ^ 2 := by    simp [sq_eLpNorm_two]  _ ≤ ∑' n : ℤ, (2 ^ 8 * eLpNorm g 2 (volume.restrict (Ioc (n - 1) (n + 2)))) ^ 2 := by    gcongr with n    apply eLpNorm_czOperator_restrict hr hg  _ = 2 ^ 16 * ∑' n : ℤ, ∫⁻ x in Ioc (n - 1 : ℝ) (n + 2), ‖g x‖ₑ ^ 2 := by    simp only [mul_pow, ← pow_mul, Nat.reduceMul, ENNReal.tsum_mul_left, sq_eLpNorm_two]  _ = 2 ^ 16 * ∑' n : ℤ, ((∫⁻ x in Ioc (n - 1 : ℝ) n, ‖g x‖ₑ ^ 2) +      (∫⁻ x in Ioc (n : ℝ) (n + 1), ‖g x‖ₑ ^ 2) + ∫⁻ x in Ioc (n + 1 : ℝ) (n + 2), ‖g x‖ₑ ^ 2) := by    congr with n    rw [← lintegral_union measurableSet_Ioc (Ioc_disjoint_Ioc_of_le le_rfl)]    simp only [tsub_le_iff_right, le_add_iff_nonneg_right, zero_le_one, Ioc_union_Ioc_eq_Ioc]    rw [← lintegral_union measurableSet_Ioc (Ioc_disjoint_Ioc_of_le le_rfl)]    rw [Ioc_union_Ioc_eq_Ioc] <;> linarith  _ = 2 ^ 16 * ((∑' n : ℤ, ∫⁻ x in Ioc (n - 1 : ℝ) n, ‖g x‖ₑ ^ 2) +        (∑' n : ℤ, ∫⁻ x in Ioc (n : ℝ) (n + 1), ‖g x‖ₑ ^ 2) +        (∑' n : ℤ, ∫⁻ x in Ioc (n + 1 : ℝ) (n + 2), ‖g x‖ₑ ^ 2)) := by simp [ENNReal.tsum_add]  _ = 2 ^ 16 * ((∑' n : ℤ, ∫⁻ x in Ioc (n : ℝ) (n + 1), ‖g x‖ₑ ^ 2) +        (∑' n : ℤ, ∫⁻ x in Ioc (n : ℝ) (n + 1), ‖g x‖ₑ ^ 2) +        (∑' n : ℤ, ∫⁻ x in Ioc (n : ℝ) (n + 1), ‖g x‖ₑ ^ 2)) := by    congr 2    · rw [← (Equiv.addRight 1).tsum_eq]      simp    · rw [← (Equiv.subRight 1).tsum_eq]      simp only [Equiv.subRight_apply, Int.cast_sub, Int.cast_one, sub_add_cancel]      ring_nf  _ = 2 ^ 16 * (3 * (eLpNorm g 2) ^ 2) := by    simp only [sq_eLpNorm_two]    conv_rhs => rw [A, lintegral_sum_measure]    ring  _ ≤ 2 ^ 18 * (eLpNorm g 2 volume) ^ 2 := by    rw [← mul_assoc]    gcongr    norm_num