cotlar_set_F₁

theorem cotlar_set_F₁ (hr : 0 < r) (hR : r ≤ R) {g : X → ℂ} (hg : BoundedFiniteSupport g) :    volume.restrict (ball x (R / 4))      {x' | 4 * globalMaximalFunction volume 1 (czOperator K r g) x < ‖czOperator K r g x'‖ₑ } ≤    volume (ball x (R / 4)) / 4 := by  let MTrgx := globalMaximalFunction volume 1 (czOperator K r g) x  by_cases hMzero : MTrgx = 0  · apply le_of_eq_of_le _ zero_le    rw [measure_eq_zero_iff_ae_notMem]    have czzero := globalMaximalFunction_zero_enorm_ae_zero (R := R / 4) (by simp [lt_of_lt_of_le hr hR]) (by fun_prop) hMzero    filter_upwards [czzero] with x' hx'    simp [hx']  rw [← lintegral_indicator_one₀ (nullMeasurableSet_lt (by fun_prop) (by fun_prop))]  by_cases hMinfty : MTrgx = ∞  · unfold MTrgx at hMinfty    simp_rw [hMinfty]    simp  rw [← ENNReal.mul_le_mul_iff_left (by simp [hMzero]) (by finiteness) (c := 4 * MTrgx)]  rw [← lintegral_mul_const' _ _ (by finiteness)]  simp_rw [← indicator_mul_const, Pi.one_apply, one_mul]  trans ∫⁻ (y : X) in ball x (R / 4),      {x' | 4 * MTrgx < ‖czOperator K r g x'‖ₑ}.indicator (fun x_1 ↦ ‖czOperator K r g y‖ₑ ) y  · apply lintegral_mono    intro y    apply indicator_le_indicator'    rw [mem_setOf_eq]    exact le_of_lt  trans ∫⁻ (y : X) in ball x (R / 4), ‖czOperator K r g y‖ₑ  · apply lintegral_mono    intro y    apply indicator_le_self  nth_rw 2 [div_eq_mul_inv]  rw [mul_assoc]  nth_rw 2 [← mul_assoc]  rw [ENNReal.inv_mul_cancel (by simp) (by simp)]  simp only [one_mul, MTrgx]  apply lintegral_ball_le_volume_mul_globalMaximalFunction  simp [(lt_of_lt_of_le hr hR)]