monotone_lcoConvergent

lemma monotone_lcoConvergent : Monotone (lcoConvergent K Q f) := fun i j hl x ↦ by  refine iSup₂_le fun R₁ mR₁ ↦ iSup₂_le fun R₂ mR₂ ↦ ?_  have lb : (2 ^ j : ℝ)⁻¹ ≤ (2 ^ i)⁻¹ := inv_pow_le_inv_pow_of_le one_le_two hl  have ub : (2 ^ i : ℝ) ≤ 2 ^ j := pow_le_pow_right₀ one_le_two hl  have mR₁' : R₁ ∈ Ioo (2 ^ j)⁻¹ (2 ^ j) := Ioo_subset_Ioo lb ub mR₁  have mR₂' : R₂ ∈ Ioo R₁ (2 ^ j) := Ioo_subset_Ioo le_rfl ub mR₂  calc    _ ≤ ‖T_R K Q R₁ R₂ (2 ^ j) f x‖ₑ := by      simp_rw [T_R, enorm_indicator_eq_indicator_enorm]      exact indicator_le_indicator_of_subset (Metric.ball_subset_ball ub) zero_le _    _ ≤ ⨆ R₂ ∈ Ioo R₁ (2 ^ j), ‖T_R K Q R₁ R₂ (2 ^ j) f x‖ₑ := by apply le_biSup _ mR₂'    _ ≤ _ := by apply le_biSup _ mR₁'