lintegral_inv_vol_le

lemma lintegral_inv_vol_le {R₁ R₂ : ℝ≥0} (hR₁ : 0 < R₁) (hR₂ : R₁ < R₂) :    ∫⁻ y in Annulus.oo x R₁ R₂, (vol x y)⁻¹ ≤ ↑((2 * R₂ / R₁) ^ a) := by  suffices ∀ y ∈ Annulus.oo x R₁ R₂, volume (ball x R₂) / ↑((2 * R₂ / R₁) ^ a) ≤ vol x y by    calc      _ ≤ ∫⁻ y in Annulus.oo x R₁ R₂, ↑((2 * R₂ / R₁) ^ a) / volume (ball x R₂) := by        refine setLIntegral_mono' Annulus.measurableSet_oo fun y my ↦ ?_        rw [← ENNReal.inv_div (.inr measure_ball_ne_top)]; swap        · exact .inr (measure_ball_pos _ _ (hR₁.trans hR₂)).ne'        rw [ENNReal.inv_le_inv]; exact this y my      _ ≤ ↑((2 * R₂ / R₁) ^ a) / volume (ball x R₂) * volume (ball x R₂) := by        rw [setLIntegral_const]; gcongr; intro y my; rw [Annulus.oo_eq] at my; exact my.1      _ = _ :=        ENNReal.div_mul_cancel (measure_ball_pos _ _ (hR₁.trans hR₂)).ne' measure_ball_ne_top  intro y my  obtain ⟨n, _, _⟩ : ∃ n, R₂ ≤ 2 ^ n * dist x y ∧ 2 ^ n ≤ 2 * R₂ / R₁ := by    have : 1 ≤ R₂ / R₁ := by rw [one_le_div hR₁]; exact hR₂.le    obtain ⟨n, hn₁, hn₂⟩ := exists_nat_pow_near this one_lt_two; use n + 1; constructor    · rw [div_lt_iff₀ hR₁, ← NNReal.coe_lt_coe, NNReal.coe_mul, NNReal.coe_pow,        NNReal.coe_ofNat] at hn₂      rw [Annulus.oo, mem_setOf, mem_Ioo] at my; apply hn₂.le.trans; gcongr; exact my.1.le    · rw [pow_succ', mul_div_assoc]; gcongr  calc    _ ≤ volume (ball x (2 ^ n * dist x y)) / (2 ^ a) ^ n := by      rw [← pow_mul, show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl, ← coe_pow, mul_comm a, pow_mul]; gcongr    _ ≤ _ := by      apply ENNReal.div_le_of_le_mul'      convert! measure_ball_two_le_same_iterate (μ := volume) x (dist x y) n; norm_cast