norm_sub_indicator_k

lemma norm_sub_indicator_k {x r : ℝ} (hxr : r ≤ |x|) (hxpi : |x| ≤ π) (hr : 0 < r) (h'r : r < 1) :    ‖(1 - exp (I * x))⁻¹ - {y | |y| ∈ Ico r 1}.indicator k x‖ ≤ 2 * niceKernel r x := by  rcases lt_or_ge (|x|) 1 with h'x | h'x  · rw [indicator_of_mem]; swap    · exact ⟨hxr, h'x⟩    have : (1 - exp (I * x))⁻¹ - k x = (1 - exp (I * x))⁻¹ * |x| := by      have : max (1 - |x|) 0 = 1 - |x| := by simpa using h'x.le      simp [k, this, div_eq_inv_mul]      ring    simp only [this, Complex.norm_mul, norm_inv, norm_real, Real.norm_eq_abs, abs_abs, ge_iff_le]    calc    ‖1 - exp (I * x)‖⁻¹ * |x|    _ ≤ (|x| / 2) ⁻¹ * |x| := by      gcongr      · linarith      · apply lower_secant_bound _ le_rfl        have := abs_le.1 hxpi        simp only [neg_mul, mem_Icc, neg_add_le_iff_le_add]        exact ⟨by linarith, by linarith⟩    _ = 2 * 1 := by      have := hr.trans_le hxr      field_simp    _ ≤ 2 * niceKernel r x := by      gcongr      exact one_le_niceKernel hr h'r  · rw [indicator_of_notMem]; swap    · simp [h'x]    simp only [sub_zero, norm_inv]    calc    ‖1 - exp (I * x)‖⁻¹    _ ≤ (|x| / 2) ⁻¹ := by      gcongr      apply lower_secant_bound _ le_rfl      have := abs_le.1 hxpi      simp only [neg_mul, mem_Icc, neg_add_le_iff_le_add]      exact ⟨by linarith, by linarith⟩    _ ≤ (1 / 2) ⁻¹ := by      gcongr    _ = 2 * 1 := by norm_num    _ ≤ 2 * niceKernel r x := by      gcongr      exact one_le_niceKernel hr h'r