estimate_x_shift

theorem estimate_x_shift (ha : 4 ≤ a)    {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : 0 < r) (hx : dist x x' ≤ r) :    edist (czOperator K r g x) (czOperator K r g x') ≤    C10_1_2 a * globalMaximalFunction volume 1 g x := by  let bxrc := (ball x r)ᶜ  let bx2r := ball x (2*r)  let bxprc := (ball x' r)ᶜ  -- Domain split x integral  have dom_x : bxrc = (bxrc ∩ bx2r) ∪ bx2rᶜ := by    conv_lhs =>      rw [← inter_univ bxrc, ← union_compl_self bx2r, inter_union_distrib_left]    congr    symm    rw [right_eq_inter, compl_subset_compl]    exact ball_subset_ball (by linarith)  have ball2_sub_ballprime : bx2rᶜ ⊆ bxprc := by    rw [compl_subset_compl]    apply ball_subset    rw [dist_comm]    apply hx.trans    linarith  -- Domain split x' integral  have dom_x_prime : bxprc = (bxprc ∩ bx2r) ∪ bx2rᶜ := by    rw [right_eq_inter.mpr ball2_sub_ballprime]    exact (inter_union_compl bxprc bx2r).symm  -- Integral split x  have integral_x : czOperator K r g x = (∫ y in (bxrc ∩ bx2r), K x y * g y) + (∫ y in bx2rᶜ, K x y * g y) := by    calc czOperator K r g x      _ = (∫ y in bxrc, K x y * g y) := by rfl      _ = (∫ y in (bxrc ∩ bx2r) ∪ bx2rᶜ , K x y * g y) := by nth_rw 1 [dom_x]    apply setIntegral_union_2    · rw [disjoint_compl_right_iff_subset]      exact inter_subset_right    · exact measurableSet_ball.compl    · rw [← dom_x]      apply czOperator_welldefined hg hr  -- Integral split x'  have integral_x_prime : czOperator K r g x' = (∫ y in (bxprc ∩ bx2r), K x' y * g y) + (∫ y in bx2rᶜ, K x' y * g y) := by    calc czOperator K r g x'      _ = (∫ y in bxprc, K x' y * g y) := by rfl      _ = (∫ y in (bxprc ∩ bx2r) ∪ bx2rᶜ , K x' y * g y) := by nth_rw 1 [dom_x_prime]    refine setIntegral_union_2 ?_ measurableSet_ball.compl ?_    · rw [disjoint_compl_right_iff_subset]      exact inter_subset_right    · rw [← dom_x_prime]      exact czOperator_welldefined hg hr ..  rw [edist_eq_enorm_sub, integral_x, integral_x_prime]  -- Rewrite lhs according to 10.1.234 split  conv =>    lhs; arg 1    calc _      _ = (∫ (y : X) in bxrc ∩ bx2r, K x y * g y)                + ((∫ (y : X) in bx2rᶜ, K x y * g y) - (∫ (y : X) in bx2rᶜ, K x' y * g y))                - (∫ (y : X) in bxprc ∩ bx2r, K x' y * g y) := by ring      _ = (∫ (y : X) in bxrc ∩ bx2r, K x y * g y)                + (∫ (y : X) in bx2rᶜ, K x y * g y - K x' y * g y)                - (∫ (y : X) in bxprc ∩ bx2r, K x' y * g y) := by          rw[← integral_sub]          · apply czOperator_welldefined hg (mul_pos zero_lt_two hr)          · apply IntegrableOn.mono_set (hst := ball2_sub_ballprime)            apply czOperator_welldefined hg hr  apply enorm_sub_le.trans  trans ‖∫ (y : X) in bxrc ∩ bx2r, K x y * g y‖ₑ + ‖∫ (y : X) in bx2rᶜ, K x y * g y - K x' y * g y‖ₑ +      ‖∫ (y : X) in bxprc ∩ bx2r, K x' y * g y‖ₑ  · gcongr    apply enorm_add_le  trans (∫⁻ (y : X) in bxrc ∩ bx2r, ‖K x y * g y‖ₑ) + ‖∫ (y : X) in bx2rᶜ, K x y * g y - K x' y * g y‖ₑ +      ∫⁻ (y : X) in bxprc ∩ bx2r, ‖K x' y * g y‖ₑ  · refine add_le_add_three ?_ (by rfl) ?_ <;> apply enorm_integral_le_lintegral_enorm  -- LHS is now 10.1.234, apply respective estimates  trans (2 ^ (a ^ 3 + a) * globalMaximalFunction volume 1 g x) + (2 ^ (a ^ 3 + 2 * a) * globalMaximalFunction volume 1 g x) +      (2 ^ (a ^ 3 + 2 * a) * globalMaximalFunction volume 1 g x)  · exact add_le_add_three (estimate_10_1_2 hg hr) (estimate_10_1_3 ha hg hr hx)      (estimate_10_1_4 hg hr hx)  rw [← distrib_three_right]  gcongr  -- Now it is unavoidable to unfold C10_1_2  with_unfolding_all simp only [C10_1_2]  norm_cast  trans 2 ^ (a ^ 3 + 2 * a + 1) + 2 ^ (a ^ 3 + 2 * a) + 2 ^ (a ^ 3 + 2 * a)  · apply Nat.add_le_add_iff_right.mpr    apply Nat.add_le_add_iff_right.mpr    rw [Nat.pow_le_pow_iff_right (h := Nat.one_lt_two)]    linarith  apply le_of_eq  ring