Complex.CartanBound.exists_radius_Ioc_sum_mul_phi_div_le_Cφ_mul_sum_avoid

lemma exists_radius_Ioc_sum_mul_phi_div_le_Cφ_mul_sum_avoid    {ι : Type} (s : Finset ι) (w : ι → ℝ) (a : ι → ℝ)    (hw : ∀ i ∈ s, 0 ≤ w i) (ha : ∀ i ∈ s, 0 < a i)    (bad : Finset ℝ) {R : ℝ} (hR : 0 < R) :    ∃ r ∈ Set.Ioc R (2 * R), r ∉ bad ∧      (∑ i ∈ s, w i * φ (r / a i)) ≤ Cφ * (∑ i ∈ s, w i) := by  by_contra hbad  have hforall :      ∀ r ∈ Set.Ioc R (2 * R), r ∉ bad →        Cφ * (∑ i ∈ s, w i) < (∑ i ∈ s, w i * φ (r / a i)) := by    intro r hr hrbad    have : ¬(∑ i ∈ s, w i * φ (r / a i)) ≤ Cφ * (∑ i ∈ s, w i) := by      intro hle      exact hbad ⟨r, hr, hrbad, hle⟩    exact lt_of_not_ge this  let g : ℝ → ℝ := ∑ i ∈ s, fun r : ℝ => w i * φ (r / a i)  have hg_int : IntervalIntegrable g volume R (2 * R) := by    simpa [g] using intervalIntegrable_sum_mul_phi_div s w a ha hR.le  have hconst_int :      IntervalIntegrable (fun _r : ℝ => Cφ * (∑ i ∈ s, w i)) volume R (2 * R) :=    intervalIntegrable_const  have hlt_meas :      (volume.restrict (Set.Ioc R (2 * R)))        {r | Cφ * (∑ i ∈ s, w i) < g r} ≠ 0 := by    have hall : Set.Ioc R (2 * R) \ (bad : Set ℝ) ⊆ {r | Cφ * (∑ i ∈ s, w i) < g r} := by      intro r hr      have hrIoc : r ∈ Set.Ioc R (2 * R) := hr.1      have hrbad : r ∉ bad := by simpa using hr.2      simpa [g] using hforall r hrIoc hrbad    have hle :        (volume.restrict (Set.Ioc R (2 * R))) (Set.Ioc R (2 * R) \ (bad : Set ℝ))          ≤ (volume.restrict (Set.Ioc R (2 * R))) {r | Cφ * (∑ i ∈ s, w i) < g r} :=      MeasureTheory.measure_mono hall    have hpos' :        (volume.restrict (Set.Ioc R (2 * R))) (Set.Ioc R (2 * R) \ (bad : Set ℝ)) ≠ 0 := by      exact restrict_volume_Ioc_two_mul_diff_finset_ne_zero bad hR    intro hzero    have : (volume.restrict (Set.Ioc R (2 * R))) (Set.Ioc R (2 * R) \ (bad : Set ℝ)) = 0 :=      le_antisymm (le_trans hle (le_of_eq hzero)) (by positivity)    exact hpos' this  have hlt_int :      (∫ r in R..(2 * R), (Cφ * (∑ i ∈ s, w i)) ∂volume)        < ∫ r in R..(2 * R), g r ∂volume := by    have hab : R ≤ 2 * R := by nlinarith [hR.le]    refine intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero (μ := volume)      (a := R) (b := 2 * R) (f := fun _ => (Cφ * (∑ i ∈ s, w i))) (g := g)      hab hconst_int hg_int ?_ hlt_meas    have hmem : ∀ᵐ r ∂ (volume.restrict (Set.Ioc R (2 * R))), r ∈ Set.Ioc R (2 * R) :=      MeasureTheory.ae_restrict_mem (by simp)    have hnotBad :        ∀ᵐ r ∂ (volume.restrict (Set.Ioc R (2 * R))), r ∉ (bad : Set ℝ) := by      simpa using        (bad.finite_toSet.countable.ae_notMem (μ := (volume.restrict (Set.Ioc R (2 * R)))))    filter_upwards [hmem, hnotBad] with r hrIoc hrNotBad    have hrNotBad' : r ∉ bad := by simpa using hrNotBad    exact le_of_lt (by simpa [g] using hforall r hrIoc hrNotBad')  have hconst_eval :      (∫ r in R..(2 * R), (Cφ * (∑ i ∈ s, w i)) ∂volume) = Cφ * (∑ i ∈ s, w i) * R := by    simp [intervalIntegral.integral_const, sub_eq_add_neg, mul_comm]    ring  have hg_le :      (∫ r in R..(2 * R), g r ∂volume) ≤ Cφ * (∑ i ∈ s, w i) * R := by    simpa [g] using integral_sum_mul_phi_div_le_Cφ_mul_sum s w a hw ha hR.le  have : ¬(Cφ * (∑ i ∈ s, w i) * R < Cφ * (∑ i ∈ s, w i) * R) := lt_irrefl _  have hcontra : Cφ * (∑ i ∈ s, w i) * R < Cφ * (∑ i ∈ s, w i) * R := by    have := hlt_int    simpa [hconst_eval] using (this.trans_le hg_le)  exact this hcontra