α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
let q : ℕ → Prop := fun i => p i ∧ 0 < r i
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
h₂ : blimsup (fun i => thickening (M * r i) (s i)) atTop p = blimsup (fun i => thickening (M * r i) (s i)) atTop q
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop q =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop q
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
h₂ : blimsup (fun i => thickening (M * r i) (s i)) atTop p = blimsup (fun i => thickening (M * r i) (s i)) atTop q
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop p
rw [h₁, h₂]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
h₂ : blimsup (fun i => thickening (M * r i) (s i)) atTop p = blimsup (fun i => thickening (M * r i) (s i)) atTop q
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop q =ᵐ[μ] blimsup (fun i => thickening (r i) (s i)) atTop q
exact blimsup_thickening_mul_ae_eq_aux μ q s hM r hr (eventually_of_forall fun i hi => hi.2)
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
i : ℕ
h : thickening (r i) (s i) ≠ ⊥
⊢ p i ↔ q i
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
⊢ blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
refine' blimsup_congr' (eventually_of_forall fun i h => _)
case hi
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
i : ℕ
h : thickening (r i) (s i) ≠ ⊥
⊢ 0 < r i

α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
i : ℕ
h : thickening (r i) (s i) ≠ ⊥
hi : 0 < r i
⊢ p i ↔ q i
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
i : ℕ
h : thickening (r i) (s i) ≠ ⊥
⊢ p i ↔ q i
replace hi : 0 < r i
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
i : ℕ
h : thickening (r i) (s i) ≠ ⊥
hi : 0 < r i
⊢ p i ↔ q i
simp only [hi, iff_self_and, imp_true_iff]
case hi
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
i : ℕ
h : r i ≤ 0
⊢ thickening (r i) (s i) = ⊥
case hi
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
i : ℕ
h : thickening (r i) (s i) ≠ ⊥
⊢ 0 < r i
contrapose! h
no goals
case hi
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
i : ℕ
h : r i ≤ 0
⊢ thickening (r i) (s i) = ⊥
apply thickening_of_nonpos h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : thickening (M * r i) (s i) ≠ ⊥
⊢ p i ↔ q i
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p = blimsup (fun i => thickening (M * r i) (s i)) atTop q
refine' blimsup_congr' (eventually_of_forall fun i h => _)
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : thickening (M * r i) (s i) ≠ ⊥
⊢ 0 < r i

α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : 0 < r i
⊢ p i ↔ q i
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : thickening (M * r i) (s i) ≠ ⊥
⊢ p i ↔ q i
replace h : 0 < r i
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : 0 < r i
⊢ p i ↔ q i
simp only [h, iff_self_and, imp_true_iff]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : thickening (M * r i) (s i) ≠ ⊥
⊢ 0 < M * r i
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : thickening (M * r i) (s i) ≠ ⊥
⊢ 0 < r i
rw [← zero_lt_mul_left hM]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : M * r i ≤ 0
⊢ thickening (M * r i) (s i) = ⊥
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : thickening (M * r i) (s i) ≠ ⊥
⊢ 0 < M * r i
contrapose! h
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : MeasureTheory.Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : M * r i ≤ 0
⊢ thickening (M * r i) (s i) = ⊥
apply thickening_of_nonpos h