RS_prime.support_pre413

lemma support_pre413 {f : ℝ → ℝ} {x : ℝ} (hx : 2 ≤ x) :  (Function.support fun (n: ℕ) ↦ ∫ (x : ℝ) in ↑n..↑n + 1, f x ∂«θ».Stieltjes.measure.restrict (Set.Icc 2 x)) ⊆    (Finset.Ico 1 ⌊x⌋₊) := by  intro n hn  simp only [Function.mem_support, ne_eq] at hn  rw [intervalIntegral.integral_of_le (by simp), ← ne_eq, ← abs_pos] at hn  grw [MeasureTheory.abs_integral_le_integral_abs] at hn  rw [MeasureTheory.integral_pos_iff_support_of_nonneg_ae] at hn  · simp only [measurableSet_Ioc, Measure.restrict_restrict, measurableSet_Icc,      MeasurableSet.inter, Measure.restrict_apply'] at hn    by_cases n_eq: n = 0    · simp only [n_eq, CharP.cast_eq_zero, zero_add] at hn      conv at hn =>        pattern _ ∩ _        rhs        equals ∅ => grind      simp at hn    by_contra!    conv at hn =>      rhs      arg 2      rhs      equals (Set.Ioc ↑n x) =>        ext a        simp only [Set.mem_inter_iff, Set.mem_Ioc, Set.mem_Icc]        refine ⟨?_, ?_⟩        · intro ha          refine ⟨by grind, ?_⟩          grind        · intro ha          simp only [coe_Ico, Set.mem_Ico, not_and_or] at this          refine ⟨?_, ?_⟩          · refine ⟨?_, ?_⟩            · grind            · cases this              · grind              · rename_i n_le                simp at n_le                grw [ha.2]                grw [Nat.lt_floor_add_one (a := x)]                simpa using n_le          · refine ⟨?_, by grind⟩            have le_x: (2: ℕ) ≤ x := by norm_cast            apply Nat.le_floor at le_x            conv =>              lhs              equals ↑(2: ℕ) => simp             simp only [not_le, lt_one_iff, n_eq, not_lt, false_or] at this            grw [le_x, this]            linarith     apply _root_.ne_of_lt at hn    rw [ne_eq, eq_comm] at hn    rw [measure_inter_null_of_null_right] at hn    · simp at hn    · simp only [«θ».Stieltjes, StieltjesFunction.measure_Ioc, ENNReal.ofReal_eq_zero, tsub_le_iff_right, zero_add]      rw [theta_eq_theta_coe_floor]      apply Monotone.imp (by exact theta_mono)      simp only [coe_Ico, Set.mem_Ico, not_and, not_lt] at this      simp [this (by omega)]  · apply Filter.Eventually.of_forall    intro y    simp  · apply MeasureTheory.Integrable.of_integral_ne_zero    grind