[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : SeminormedAddCommGroup E
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => ↑↑μ {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
[PROOFSTEP]
simp_rw [TendstoInMeasure, dist_eq_norm]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
⊢ TendstoInMeasure μ f' l g'
[PROOFSTEP]
intro ε hε
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) l (𝓝 0)
[PROOFSTEP]
suffices (fun i => μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => μ {x | ε ≤ dist (f i x) (g x)}
  by
  rw [tendsto_congr' this]
  exact h_tendsto ε hε
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
this : (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) l (𝓝 0)
[PROOFSTEP]
rw [tendsto_congr' this]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
this : (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
[PROOFSTEP]
exact h_tendsto ε hε
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}
[PROOFSTEP]
filter_upwards [h_left] with i h_ae_eq
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
⊢ ↑↑μ {x | ε ≤ dist (f' i x) (g' x)} = ↑↑μ {x | ε ≤ dist (f i x) (g x)}
[PROOFSTEP]
refine' measure_congr _
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
⊢ {x | ε ≤ dist (f' i x) (g' x)} =ᵐ[μ] {x | ε ≤ dist (f i x) (g x)}
[PROOFSTEP]
filter_upwards [h_ae_eq, h_right] with x hxf hxg
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ setOf (fun x => ε ≤ dist (f' i x) (g' x)) x = setOf (fun x => ε ≤ dist (f i x) (g x)) x
[PROOFSTEP]
rw [eq_iff_iff]
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ setOf (fun x => ε ≤ dist (f' i x) (g' x)) x ↔ setOf (fun x => ε ≤ dist (f i x) (g x)) x
[PROOFSTEP]
change ε ≤ dist (f' i x) (g' x) ↔ ε ≤ dist (f i x) (g x)
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ ε ≤ dist (f' i x) (g' x) ↔ ε ≤ dist (f i x) (g x)
[PROOFSTEP]
rw [hxg, hxf]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ TendstoInMeasure μ f atTop g
[PROOFSTEP]
refine' fun ε hε => ENNReal.tendsto_atTop_zero.mpr fun δ hδ => _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ δ
[PROOFSTEP]
by_cases hδi : δ = ∞
[GOAL]
case pos
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
hδi : δ = ⊤
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ δ
[PROOFSTEP]
simp only [hδi, imp_true_iff, le_top, exists_const]
[GOAL]
case neg
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
hδi : ¬δ = ⊤
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ δ
[PROOFSTEP]
lift δ to ℝ≥0 using hδi
[GOAL]
case neg.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : ↑δ > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
[PROOFSTEP]
rw [gt_iff_lt, ENNReal.coe_pos, ← NNReal.coe_pos] at hδ
[GOAL]
case neg.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
[PROOFSTEP]
obtain ⟨t, _, ht, hunif⟩ := tendstoUniformlyOn_of_ae_tendsto' hf hg hfg hδ
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ENNReal.ofReal ↑δ
hunif : TendstoUniformlyOn (fun n => f n) g atTop tᶜ
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
[PROOFSTEP]
rw [ENNReal.ofReal_coe_nnreal] at ht
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : TendstoUniformlyOn (fun n => f n) g atTop tᶜ
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
[PROOFSTEP]
rw [Metric.tendstoUniformlyOn_iff] at hunif
[GOAL]
case neg.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
[PROOFSTEP]
obtain ⟨N, hN⟩ := eventually_atTop.1 (hunif ε hε)
[GOAL]
case neg.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
[PROOFSTEP]
refine' ⟨N, fun n hn => _⟩
[GOAL]
case neg.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
[PROOFSTEP]
suffices : {x : α | ε ≤ dist (f n x) (g x)} ⊆ t
[GOAL]
case neg.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
this : {x | ε ≤ dist (f n x) (g x)} ⊆ t
⊢ ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
case this
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ {x | ε ≤ dist (f n x) (g x)} ⊆ t
[PROOFSTEP]
exact (measure_mono this).trans ht
[GOAL]
case this
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ {x | ε ≤ dist (f n x) (g x)} ⊆ t
[PROOFSTEP]
rw [← Set.compl_subset_compl]
[GOAL]
case this
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ tᶜ ⊆ {x | ε ≤ dist (f n x) (g x)}ᶜ
[PROOFSTEP]
intro x hx
[GOAL]
case this
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ x ∈ {x | ε ≤ dist (f n x) (g x)}ᶜ
[PROOFSTEP]
rw [Set.mem_compl_iff, Set.nmem_setOf_iff, dist_comm, not_le]
[GOAL]
case this
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ dist (g x) (f n x) < ε
[PROOFSTEP]
exact hN n hn x hx
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ TendstoInMeasure μ f atTop g
[PROOFSTEP]
have hg : AEStronglyMeasurable g μ := aestronglyMeasurable_of_tendsto_ae _ hf hfg
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ TendstoInMeasure μ f atTop g
[PROOFSTEP]
refine' TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ TendstoInMeasure μ (fun i => AEStronglyMeasurable.mk (f i) (_ : AEStronglyMeasurable (f i) μ)) atTop
    (AEStronglyMeasurable.mk g hg)
[PROOFSTEP]
refine'
  tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable (fun i => (hf i).stronglyMeasurable_mk) hg.stronglyMeasurable_mk
    _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (fun n => AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x) atTop
      (𝓝 (AEStronglyMeasurable.mk g hg x))
[PROOFSTEP]
have hf_eq_ae : ∀ᵐ x ∂μ, ∀ n, (hf n).mk (f n) x = f n x := ae_all_iff.mpr fun n => (hf n).ae_eq_mk.symm
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (fun n => AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x) atTop
      (𝓝 (AEStronglyMeasurable.mk g hg x))
[PROOFSTEP]
filter_upwards [hf_eq_ae, hg.ae_eq_mk, hfg] with x hxf hxg hxfg
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun n => AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x) atTop
    (𝓝 (AEStronglyMeasurable.mk g hg x))
[PROOFSTEP]
rw [← hxg, funext fun n => hxf n]
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun n => f n x) atTop (𝓝 (g x))
[PROOFSTEP]
exact hxfg
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ ∃ N, ∀ (m_1 : ℕ), m_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n
[PROOFSTEP]
specialize hfg ((2⁻¹ : ℝ) ^ n) (by simp only [Real.rpow_nat_cast, inv_pos, zero_lt_two, pow_pos])
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ 0 < 2⁻¹ ^ n
[PROOFSTEP]
simp only [Real.rpow_nat_cast, inv_pos, zero_lt_two, pow_pos]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : Tendsto (fun i => ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f i x) (g x)}) atTop (𝓝 0)
⊢ ∃ N, ∀ (m_1 : ℕ), m_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n
[PROOFSTEP]
rw [ENNReal.tendsto_atTop_zero] at hfg
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n_1 : ℕ), n_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f n_1 x) (g x)} ≤ ε
⊢ ∃ N, ∀ (m_1 : ℕ), m_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n
[PROOFSTEP]
exact hfg ((2 : ℝ≥0∞)⁻¹ ^ n) (pos_iff_ne_zero.mpr fun h_zero => by simpa using pow_eq_zero h_zero)
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n_1 : ℕ), n_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f n_1 x) (g x)} ≤ ε
h_zero : 2⁻¹ ^ n = 0
⊢ False
[PROOFSTEP]
simpa using pow_eq_zero h_zero
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ seqTendstoAeSeq hfg (n + 1) = max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)
[PROOFSTEP]
rw [seqTendstoAeSeq]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n k : ℕ
hn : seqTendstoAeSeq hfg n ≤ k
⊢ ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k : ℕ
hn : seqTendstoAeSeq hfg Nat.zero ≤ k
⊢ ↑↑μ {x | 2⁻¹ ^ Nat.zero ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ Nat.zero
[PROOFSTEP]
exact Classical.choose_spec (exists_nat_measure_lt_two_inv hfg 0) k hn
[GOAL]
case succ
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k n✝ : ℕ
hn : seqTendstoAeSeq hfg (Nat.succ n✝) ≤ k
⊢ ↑↑μ {x | 2⁻¹ ^ Nat.succ n✝ ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ Nat.succ n✝
[PROOFSTEP]
exact Classical.choose_spec (exists_nat_measure_lt_two_inv hfg _) _ (le_trans (le_max_left _ _) hn)
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
⊢ StrictMono (seqTendstoAeSeq hfg)
[PROOFSTEP]
refine' strictMono_nat_of_lt_succ fun n => _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ seqTendstoAeSeq hfg n < seqTendstoAeSeq hfg (n + 1)
[PROOFSTEP]
rw [seqTendstoAeSeq_succ]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ seqTendstoAeSeq hfg n < max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)
[PROOFSTEP]
exact lt_of_lt_of_le (lt_add_one <| seqTendstoAeSeq hfg n) (le_max_right _ _)
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
have h_lt_ε_real : ∀ (ε : ℝ) (_ : 0 < ε), ∃ k : ℕ, 2 * (2 : ℝ)⁻¹ ^ k < ε :=
  by
  intro ε hε
  obtain ⟨k, h_k⟩ : ∃ k : ℕ, (2 : ℝ)⁻¹ ^ k < ε := exists_pow_lt_of_lt_one hε (by norm_num)
  refine' ⟨k + 1, (le_of_eq _).trans_lt h_k⟩
  rw [pow_add]; ring
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
⊢ ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
[PROOFSTEP]
intro ε hε
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ
hε : 0 < ε
⊢ ∃ k, 2 * 2⁻¹ ^ k < ε
[PROOFSTEP]
obtain ⟨k, h_k⟩ : ∃ k : ℕ, (2 : ℝ)⁻¹ ^ k < ε := exists_pow_lt_of_lt_one hε (by norm_num)
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ
hε : 0 < ε
⊢ 2⁻¹ < 1
[PROOFSTEP]
norm_num
[GOAL]
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ
hε : 0 < ε
k : ℕ
h_k : 2⁻¹ ^ k < ε
⊢ ∃ k, 2 * 2⁻¹ ^ k < ε
[PROOFSTEP]
refine' ⟨k + 1, (le_of_eq _).trans_lt h_k⟩
[GOAL]
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ
hε : 0 < ε
k : ℕ
h_k : 2⁻¹ ^ k < ε
⊢ 2 * 2⁻¹ ^ (k + 1) = 2⁻¹ ^ k
[PROOFSTEP]
rw [pow_add]
[GOAL]
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
ε : ℝ
hε : 0 < ε
k : ℕ
h_k : 2⁻¹ ^ k < ε
⊢ 2 * (2⁻¹ ^ k * 2⁻¹ ^ 1) = 2⁻¹ ^ k
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
set ns := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
use ns
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
let S := fun k => {x | (2 : ℝ)⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
have hμS_le : ∀ k, μ (S k) ≤ (2 : ℝ≥0∞)⁻¹ ^ k := by
  intro k
  have := ExistsSeqTendstoAe.seqTendstoAeSeq_spec hfg k (ns k) le_rfl
  convert this
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
⊢ ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
[PROOFSTEP]
intro k
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
k : ℕ
⊢ ↑↑μ (S k) ≤ 2⁻¹ ^ k
[PROOFSTEP]
have := ExistsSeqTendstoAe.seqTendstoAeSeq_spec hfg k (ns k) le_rfl
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
k : ℕ
this : ↑↑μ {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)} ≤ 2⁻¹ ^ k
⊢ ↑↑μ (S k) ≤ 2⁻¹ ^ k
[PROOFSTEP]
convert this
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
set s := Filter.atTop.limsup S with hs
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
have hμs : μ s = 0 :=
  by
  refine' measure_limsup_eq_zero (ne_of_lt <| lt_of_le_of_lt (ENNReal.tsum_le_tsum hμS_le) _)
  simp only [ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, inv_inv]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
⊢ ↑↑μ s = 0
[PROOFSTEP]
refine' measure_limsup_eq_zero (ne_of_lt <| lt_of_le_of_lt (ENNReal.tsum_le_tsum hμS_le) _)
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
⊢ ∑' (a : ℕ), 2⁻¹ ^ a < ⊤
[PROOFSTEP]
simp only [ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, inv_inv]
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
have h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x)) :=
  by
  refine' fun x hx => Metric.tendsto_atTop.mpr fun ε hε => _
  rw [hs, limsup_eq_iInf_iSup_of_nat] at hx
  simp only [Set.iSup_eq_iUnion, Set.iInf_eq_iInter, Set.compl_iInter, Set.compl_iUnion, Set.mem_iUnion, Set.mem_iInter,
    Set.mem_compl_iff, Set.mem_setOf_eq, not_le] at hx
  obtain ⟨N, hNx⟩ := hx
  obtain ⟨k, hk_lt_ε⟩ := h_lt_ε_real ε hε
  refine' ⟨max N (k - 1), fun n hn_ge => lt_of_le_of_lt _ hk_lt_ε⟩
  specialize hNx n ((le_max_left _ _).trans hn_ge)
  have h_inv_n_le_k : (2 : ℝ)⁻¹ ^ n ≤ 2 * (2 : ℝ)⁻¹ ^ k :=
    by
    rw [mul_comm, ← inv_mul_le_iff' (zero_lt_two' ℝ)]
    conv_lhs =>
      congr
      rw [← pow_one (2 : ℝ)⁻¹]
    rw [← pow_add, add_comm]
    exact
      pow_le_pow_of_le_one (one_div (2 : ℝ) ▸ one_half_pos.le) (inv_le_one one_le_two)
        ((le_tsub_add.trans (add_le_add_right (le_max_right _ _) 1)).trans (add_le_add_right hn_ge 1))
  exact le_trans hNx.le h_inv_n_le_k
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
⊢ ∀ (x : α), x ∈ sᶜ → Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
refine' fun x hx => Metric.tendsto_atTop.mpr fun ε hε => _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
hx : x ∈ sᶜ
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (f (ns n) x) (g x) < ε
[PROOFSTEP]
rw [hs, limsup_eq_iInf_iSup_of_nat] at hx
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
hx : x ∈ (⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), S i)ᶜ
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (f (ns n) x) (g x) < ε
[PROOFSTEP]
simp only [Set.iSup_eq_iUnion, Set.iInf_eq_iInter, Set.compl_iInter, Set.compl_iUnion, Set.mem_iUnion, Set.mem_iInter,
  Set.mem_compl_iff, Set.mem_setOf_eq, not_le] at hx
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
hx : ∃ i, ∀ (i_1 : ℕ), i_1 ≥ i → dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg i_1) x) (g x) < 2⁻¹ ^ i_1
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (f (ns n) x) (g x) < ε
[PROOFSTEP]
obtain ⟨N, hNx⟩ := hx
[GOAL]
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N : ℕ
hNx : ∀ (i : ℕ), i ≥ N → dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg i) x) (g x) < 2⁻¹ ^ i
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (f (ns n) x) (g x) < ε
[PROOFSTEP]
obtain ⟨k, hk_lt_ε⟩ := h_lt_ε_real ε hε
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N : ℕ
hNx : ∀ (i : ℕ), i ≥ N → dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg i) x) (g x) < 2⁻¹ ^ i
k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (f (ns n) x) (g x) < ε
[PROOFSTEP]
refine' ⟨max N (k - 1), fun n hn_ge => lt_of_le_of_lt _ hk_lt_ε⟩
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N : ℕ
hNx : ∀ (i : ℕ), i ≥ N → dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg i) x) (g x) < 2⁻¹ ^ i
k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
⊢ dist (f (ns n) x) (g x) ≤ 2 * 2⁻¹ ^ k
[PROOFSTEP]
specialize hNx n ((le_max_left _ _).trans hn_ge)
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg n) x) (g x) < 2⁻¹ ^ n
⊢ dist (f (ns n) x) (g x) ≤ 2 * 2⁻¹ ^ k
[PROOFSTEP]
have h_inv_n_le_k : (2 : ℝ)⁻¹ ^ n ≤ 2 * (2 : ℝ)⁻¹ ^ k :=
  by
  rw [mul_comm, ← inv_mul_le_iff' (zero_lt_two' ℝ)]
  conv_lhs =>
    congr
    rw [← pow_one (2 : ℝ)⁻¹]
  rw [← pow_add, add_comm]
  exact
    pow_le_pow_of_le_one (one_div (2 : ℝ) ▸ one_half_pos.le) (inv_le_one one_le_two)
      ((le_tsub_add.trans (add_le_add_right (le_max_right _ _) 1)).trans (add_le_add_right hn_ge 1))
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg n) x) (g x) < 2⁻¹ ^ n
⊢ 2⁻¹ ^ n ≤ 2 * 2⁻¹ ^ k
[PROOFSTEP]
rw [mul_comm, ← inv_mul_le_iff' (zero_lt_two' ℝ)]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg n) x) (g x) < 2⁻¹ ^ n
⊢ 2⁻¹ * 2⁻¹ ^ n ≤ 2⁻¹ ^ k
[PROOFSTEP]
conv_lhs =>
  congr
  rw [← pow_one (2 : ℝ)⁻¹]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg n) x) (g x) < 2⁻¹ ^ n
| 2⁻¹ * 2⁻¹ ^ n
[PROOFSTEP]
  congr
  rw [← pow_one (2 : ℝ)⁻¹]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg n) x) (g x) < 2⁻¹ ^ n
| 2⁻¹ * 2⁻¹ ^ n
[PROOFSTEP]
  congr
  rw [← pow_one (2 : ℝ)⁻¹]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg n) x) (g x) < 2⁻¹ ^ n
| 2⁻¹ * 2⁻¹ ^ n
[PROOFSTEP]
congr
[GOAL]
case a
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg n) x) (g x) < 2⁻¹ ^ n
| 2⁻¹
case a
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg n) x) (g x) < 2⁻¹ ^ n
| 2⁻¹ ^ n
[PROOFSTEP]
rw [← pow_one (2 : ℝ)⁻¹]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg n) x) (g x) < 2⁻¹ ^ n
⊢ 2⁻¹ ^ 1 * 2⁻¹ ^ n ≤ 2⁻¹ ^ k
[PROOFSTEP]
rw [← pow_add, add_comm]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg n) x) (g x) < 2⁻¹ ^ n
⊢ 2⁻¹ ^ (n + 1) ≤ 2⁻¹ ^ k
[PROOFSTEP]
exact
  pow_le_pow_of_le_one (one_div (2 : ℝ) ▸ one_half_pos.le) (inv_le_one one_le_two)
    ((le_tsub_add.trans (add_le_add_right (le_max_right _ _) 1)).trans (add_le_add_right hn_ge 1))
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
x : α
ε : ℝ
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hn_ge : n ≥ max N (k - 1)
hNx : dist (f (ExistsSeqTendstoAe.seqTendstoAeSeq hfg n) x) (g x) < 2⁻¹ ^ n
h_inv_n_le_k : 2⁻¹ ^ n ≤ 2 * 2⁻¹ ^ k
⊢ dist (f (ns n) x) (g x) ≤ 2 * 2⁻¹ ^ k
[PROOFSTEP]
exact le_trans hNx.le h_inv_n_le_k
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
h_tendsto : ∀ (x : α), x ∈ sᶜ → Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
⊢ StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
rw [ae_iff]
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
h_tendsto : ∀ (x : α), x ∈ sᶜ → Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
⊢ StrictMono ns ∧ ↑↑μ {a | ¬Tendsto (fun i => f (ns i) a) atTop (𝓝 (g a))} = 0
[PROOFSTEP]
refine' ⟨ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono hfg, measure_mono_null (fun x => _) hμs⟩
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
h_tendsto : ∀ (x : α), x ∈ sᶜ → Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
x : α
⊢ x ∈ {a | ¬Tendsto (fun i => f (ns i) a) atTop (𝓝 (g a))} → x ∈ s
[PROOFSTEP]
rw [Set.mem_setOf_eq, ← @Classical.not_not (x ∈ s), not_imp_not]
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), ↑↑μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : ↑↑μ s = 0
h_tendsto : ∀ (x : α), x ∈ sᶜ → Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
x : α
⊢ ¬x ∈ s → Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
exact h_tendsto x
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
f✝ : ℕ → α → E
g✝ : α → E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
⊢ ∃ ns, TendstoInMeasure μ (fun n => f (ns n)) atTop g
[PROOFSTEP]
obtain ⟨ns, h_tendsto_ns⟩ : ∃ ns : ℕ → ι, Tendsto ns atTop u := exists_seq_tendsto u
[GOAL]
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
f✝ : ℕ → α → E
g✝ : α → E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ns : ℕ → ι
h_tendsto_ns : Tendsto ns atTop u
⊢ ∃ ns, TendstoInMeasure μ (fun n => f (ns n)) atTop g
[PROOFSTEP]
exact ⟨ns, fun ε hε => (hfg ε hε).comp h_tendsto_ns⟩
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
f✝ : ℕ → α → E
g✝ : α → E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
⊢ ∃ ns, ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
obtain ⟨ms, hms⟩ := hfg.exists_seq_tendstoInMeasure_atTop
[GOAL]
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
f✝ : ℕ → α → E
g✝ : α → E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ms : ℕ → ι
hms : TendstoInMeasure μ (fun n => f (ms n)) atTop g
⊢ ∃ ns, ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
obtain ⟨ns, -, hns⟩ := hms.exists_seq_tendsto_ae
[GOAL]
case intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
f✝ : ℕ → α → E
g✝ : α → E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ms : ℕ → ι
hms : TendstoInMeasure μ (fun n => f (ms n)) atTop g
ns : ℕ → ℕ
hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ms (ns i)) x) atTop (𝓝 (g x))
⊢ ∃ ns, ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
[PROOFSTEP]
exact ⟨ms ∘ ns, hns⟩
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n)
h_tendsto : TendstoInMeasure μ f u g
⊢ AEMeasurable g
[PROOFSTEP]
obtain ⟨ns, hns⟩ := h_tendsto.exists_seq_tendsto_ae'
[GOAL]
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
u : Filter ι
inst✝¹ : NeBot u
inst✝ : IsCountablyGenerated u
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n)
h_tendsto : TendstoInMeasure μ f u g
ns : ℕ → ι
hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
⊢ AEMeasurable g
[PROOFSTEP]
exact aemeasurable_of_tendsto_metrizable_ae atTop (fun n => hf (ns n)) hns
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g
[PROOFSTEP]
intro ε hε
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
[PROOFSTEP]
replace hfg :=
  ENNReal.Tendsto.const_mul (Tendsto.ennrpow_const p.toReal hfg) (Or.inr <| @ENNReal.ofReal_ne_top (1 / ε ^ p.toReal))
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  Tendsto (fun b => ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f b - g) p μ ^ ENNReal.toReal p) l
    (𝓝 (ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * 0 ^ ENNReal.toReal p))
⊢ Tendsto (fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
[PROOFSTEP]
simp only [mul_zero, ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos hp_ne_zero hp_ne_top)] at hfg
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg : Tendsto (fun b => ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f b - g) p μ ^ ENNReal.toReal p) l (𝓝 0)
⊢ Tendsto (fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
[PROOFSTEP]
rw [ENNReal.tendsto_nhds_zero] at hfg ⊢
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  ∀ (ε_1 : ℝ≥0∞),
    ε_1 > 0 → ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f x - g) p μ ^ ENNReal.toReal p ≤ ε_1
⊢ ∀ (ε_1 : ℝ≥0∞), ε_1 > 0 → ∀ᶠ (x : ι) in l, ↑↑μ {x_1 | ε ≤ dist (f x x_1) (g x_1)} ≤ ε_1
[PROOFSTEP]
intro δ hδ
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  ∀ (ε_1 : ℝ≥0∞),
    ε_1 > 0 → ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f x - g) p μ ^ ENNReal.toReal p ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
⊢ ∀ᶠ (x : ι) in l, ↑↑μ {x_1 | ε ≤ dist (f x x_1) (g x_1)} ≤ δ
[PROOFSTEP]
refine' (hfg δ hδ).mono fun n hn => _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  ∀ (ε_1 : ℝ≥0∞),
    ε_1 > 0 → ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f x - g) p μ ^ ENNReal.toReal p ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f n - g) p μ ^ ENNReal.toReal p ≤ δ
⊢ ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ δ
[PROOFSTEP]
refine' le_trans _ hn
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  ∀ (ε_1 : ℝ≥0∞),
    ε_1 > 0 → ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f x - g) p μ ^ ENNReal.toReal p ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f n - g) p μ ^ ENNReal.toReal p ≤ δ
⊢ ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f n - g) p μ ^ ENNReal.toReal p
[PROOFSTEP]
rw [ENNReal.ofReal_div_of_pos (Real.rpow_pos_of_pos hε _), ENNReal.ofReal_one, mul_comm, mul_one_div,
  ENNReal.le_div_iff_mul_le _ (Or.inl ENNReal.ofReal_ne_top), mul_comm]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  ∀ (ε_1 : ℝ≥0∞),
    ε_1 > 0 → ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f x - g) p μ ^ ENNReal.toReal p ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f n - g) p μ ^ ENNReal.toReal p ≤ δ
⊢ ENNReal.ofReal (ε ^ ENNReal.toReal p) * ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ snorm (f n - g) p μ ^ ENNReal.toReal p
[PROOFSTEP]
rw [← ENNReal.ofReal_rpow_of_pos hε]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  ∀ (ε_1 : ℝ≥0∞),
    ε_1 > 0 → ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f x - g) p μ ^ ENNReal.toReal p ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f n - g) p μ ^ ENNReal.toReal p ≤ δ
⊢ ENNReal.ofReal ε ^ ENNReal.toReal p * ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ snorm (f n - g) p μ ^ ENNReal.toReal p
[PROOFSTEP]
convert mul_meas_ge_le_pow_snorm' μ hp_ne_zero hp_ne_top ((hf n).sub hg).aestronglyMeasurable (ENNReal.ofReal ε)
[GOAL]
case h.e'_3.h.e'_6.h.e'_3.h.e'_2.h.a
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  ∀ (ε_1 : ℝ≥0∞),
    ε_1 > 0 → ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f x - g) p μ ^ ENNReal.toReal p ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f n - g) p μ ^ ENNReal.toReal p ≤ δ
x✝ : α
⊢ ε ≤ dist (f n x✝) (g x✝) ↔ ENNReal.ofReal ε ≤ ↑‖(f n - g) x✝‖₊
[PROOFSTEP]
rw [dist_eq_norm, ← ENNReal.ofReal_le_ofReal_iff (norm_nonneg _), ofReal_norm_eq_coe_nnnorm]
[GOAL]
case h.e'_3.h.e'_6.h.e'_3.h.e'_2.h.a
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  ∀ (ε_1 : ℝ≥0∞),
    ε_1 > 0 → ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f x - g) p μ ^ ENNReal.toReal p ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f n - g) p μ ^ ENNReal.toReal p ≤ δ
x✝ : α
⊢ ENNReal.ofReal ε ≤ ↑‖f n x✝ - g x✝‖₊ ↔ ENNReal.ofReal ε ≤ ↑‖(f n - g) x✝‖₊
[PROOFSTEP]
exact Iff.rfl
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  ∀ (ε_1 : ℝ≥0∞),
    ε_1 > 0 → ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f x - g) p μ ^ ENNReal.toReal p ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f n - g) p μ ^ ENNReal.toReal p ≤ δ
⊢ ENNReal.ofReal (ε ^ ENNReal.toReal p) ≠ 0 ∨ snorm (f n - g) p μ ^ ENNReal.toReal p ≠ 0
[PROOFSTEP]
rw [Ne, ENNReal.ofReal_eq_zero, not_le]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  ∀ (ε_1 : ℝ≥0∞),
    ε_1 > 0 → ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f x - g) p μ ^ ENNReal.toReal p ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ ENNReal.toReal p) * snorm (f n - g) p μ ^ ENNReal.toReal p ≤ δ
⊢ 0 < ε ^ ENNReal.toReal p ∨ snorm (f n - g) p μ ^ ENNReal.toReal p ≠ 0
[PROOFSTEP]
exact Or.inl (Real.rpow_pos_of_pos hε _)
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g
[PROOFSTEP]
refine' TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ (fun i => AEStronglyMeasurable.mk (f i) (_ : AEStronglyMeasurable (f i) μ)) l
    (AEStronglyMeasurable.mk g hg)
[PROOFSTEP]
refine'
  tendstoInMeasure_of_tendsto_snorm_of_stronglyMeasurable hp_ne_zero hp_ne_top (fun i => (hf i).stronglyMeasurable_mk)
    hg.stronglyMeasurable_mk _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
⊢ Tendsto
    (fun n =>
      snorm (AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) - AEStronglyMeasurable.mk g hg) p μ)
    l (𝓝 0)
[PROOFSTEP]
have : (fun n => snorm ((hf n).mk (f n) - hg.mk g) p μ) = fun n => snorm (f n - g) p μ := by ext1 n;
  refine' snorm_congr_ae (EventuallyEq.sub (hf n).ae_eq_mk.symm hg.ae_eq_mk.symm)
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
⊢ (fun n =>
      snorm (AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) - AEStronglyMeasurable.mk g hg) p μ) =
    fun n => snorm (f n - g) p μ
[PROOFSTEP]
ext1 n
[GOAL]
case h
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
n : ι
⊢ snorm (AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) - AEStronglyMeasurable.mk g hg) p μ =
    snorm (f n - g) p μ
[PROOFSTEP]
refine' snorm_congr_ae (EventuallyEq.sub (hf n).ae_eq_mk.symm hg.ae_eq_mk.symm)
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
this :
  (fun n =>
      snorm (AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) - AEStronglyMeasurable.mk g hg) p μ) =
    fun n => snorm (f n - g) p μ
⊢ Tendsto
    (fun n =>
      snorm (AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) - AEStronglyMeasurable.mk g hg) p μ)
    l (𝓝 0)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
this :
  (fun n =>
      snorm (AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) - AEStronglyMeasurable.mk g hg) p μ) =
    fun n => snorm (f n - g) p μ
⊢ Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
[PROOFSTEP]
exact hfg
[GOAL]
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hfg : Tendsto (fun n => snorm (f n - g) ⊤ μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g
[PROOFSTEP]
intro δ hδ
[GOAL]
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hfg : Tendsto (fun n => snorm (f n - g) ⊤ μ) l (𝓝 0)
δ : ℝ
hδ : 0 < δ
⊢ Tendsto (fun i => ↑↑μ {x | δ ≤ dist (f i x) (g x)}) l (𝓝 0)
[PROOFSTEP]
simp only [snorm_exponent_top, snormEssSup] at hfg
[GOAL]
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
hfg : Tendsto (fun n => essSup (fun x => ↑‖(f n - g) x‖₊) μ) l (𝓝 0)
⊢ Tendsto (fun i => ↑↑μ {x | δ ≤ dist (f i x) (g x)}) l (𝓝 0)
[PROOFSTEP]
rw [ENNReal.tendsto_nhds_zero] at hfg ⊢
[GOAL]
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
hfg : ∀ (ε : ℝ≥0∞), ε > 0 → ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖(f x - g) x_1‖₊) μ ≤ ε
⊢ ∀ (ε : ℝ≥0∞), ε > 0 → ∀ᶠ (x : ι) in l, ↑↑μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε
[PROOFSTEP]
intro ε hε
[GOAL]
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
hfg : ∀ (ε : ℝ≥0∞), ε > 0 → ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖(f x - g) x_1‖₊) μ ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : ι) in l, ↑↑μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε
[PROOFSTEP]
specialize hfg (ENNReal.ofReal δ / 2) (ENNReal.div_pos_iff.2 ⟨(ENNReal.ofReal_pos.2 hδ).ne.symm, ENNReal.two_ne_top⟩)
[GOAL]
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖(f x - g) x_1‖₊) μ ≤ ENNReal.ofReal δ / 2
⊢ ∀ᶠ (x : ι) in l, ↑↑μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε
[PROOFSTEP]
refine' hfg.mono fun n hn => _
[GOAL]
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖(f x - g) x_1‖₊) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ↑‖(f n - g) x‖₊) μ ≤ ENNReal.ofReal δ / 2
⊢ ↑↑μ {x | δ ≤ dist (f n x) (g x)} ≤ ε
[PROOFSTEP]
simp only [true_and_iff, gt_iff_lt, ge_iff_le, zero_tsub, zero_le, zero_add, Set.mem_Icc, Pi.sub_apply] at *
[GOAL]
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖f x x_1 - g x_1‖₊) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ↑‖f n x - g x‖₊) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
⊢ ↑↑μ {x | δ ≤ dist (f n x) (g x)} ≤ ε
[PROOFSTEP]
have : essSup (fun x : α => (‖f n x - g x‖₊ : ℝ≥0∞)) μ < ENNReal.ofReal δ :=
  lt_of_le_of_lt hn (ENNReal.half_lt_self (ENNReal.ofReal_pos.2 hδ).ne.symm ENNReal.ofReal_lt_top.ne)
[GOAL]
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖f x x_1 - g x_1‖₊) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ↑‖f n x - g x‖₊) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
⊢ ↑↑μ {x | δ ≤ dist (f n x) (g x)} ≤ ε
[PROOFSTEP]
refine' ((le_of_eq _).trans (ae_lt_of_essSup_lt this).le).trans hε.le
[GOAL]
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖f x x_1 - g x_1‖₊) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ↑‖f n x - g x‖₊) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
⊢ ↑↑μ {x | δ ≤ dist (f n x) (g x)} = ↑↑μ {x | (fun y => ↑‖f n y - g y‖₊ < ENNReal.ofReal δ) x}ᶜ
[PROOFSTEP]
congr with x
[GOAL]
case e_a.h
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖f x x_1 - g x_1‖₊) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ↑‖f n x - g x‖₊) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
x : α
⊢ x ∈ {x | δ ≤ dist (f n x) (g x)} ↔ x ∈ {x | (fun y => ↑‖f n y - g y‖₊ < ENNReal.ofReal δ) x}ᶜ
[PROOFSTEP]
simp only [ENNReal.ofReal_le_iff_le_toReal ENNReal.coe_lt_top.ne, ENNReal.coe_toReal, not_lt, coe_nnnorm,
  Set.mem_setOf_eq, Set.mem_compl_iff]
[GOAL]
case e_a.h
α : Type u_1
ι : Type u_2
E✝ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E✝
p : ℝ≥0∞
f✝ : ι → α → E✝
g✝ : α → E✝
E : Type u_4
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ↑‖f x x_1 - g x_1‖₊) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ↑‖f n x - g x‖₊) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
x : α
⊢ δ ≤ dist (f n x) (g x) ↔ δ ≤ ‖f n x - g x‖
[PROOFSTEP]
rw [← dist_eq_norm (f n x) (g x)]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g
[PROOFSTEP]
by_cases hp_ne_top : p = ∞
[GOAL]
case pos
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : p = ⊤
⊢ TendstoInMeasure μ f l g
[PROOFSTEP]
subst hp_ne_top
[GOAL]
case pos
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hp_ne_zero : ⊤ ≠ 0
hfg : Tendsto (fun n => snorm (f n - g) ⊤ μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g
[PROOFSTEP]
exact tendstoInMeasure_of_tendsto_snorm_top hfg
[GOAL]
case neg
α : Type u_1
ι : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : ¬p = ⊤
⊢ TendstoInMeasure μ f l g
[PROOFSTEP]
exact tendstoInMeasure_of_tendsto_snorm_of_ne_top hp_ne_zero hp_ne_top hf hg hfg


[GOAL]
α : Type u_1
β : Type u_2
e : α ≃ β
f : Perm α
⊢ ∀ {x : α}, ↑f x ≠ x ↔ ↑(↑(permCongr e) f) (↑e x) ≠ ↑e x
[PROOFSTEP]
intro b
[GOAL]
α : Type u_1
β : Type u_2
e : α ≃ β
f : Perm α
b : α
⊢ ↑f b ≠ b ↔ ↑(↑(permCongr e) f) (↑e b) ≠ ↑e b
[PROOFSTEP]
simp only [ne_eq, permCongr_apply, symm_apply_apply, EmbeddingLike.apply_eq_iff_eq]
[GOAL]
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
⊢ ↑(derangements (Subtype p)) ≃ { f // ∀ (a : α), a ∈ fixedPoints ↑↑f → ¬p a }
[PROOFSTEP]
refine' (Perm.subtypeEquivSubtypePerm p).subtypeEquiv fun f => ⟨fun hf a hfa ha => _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
hfa : a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f)
ha : p a
⊢ False
[PROOFSTEP]
refine' hf ⟨a, ha⟩ (Subtype.ext _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
hfa : a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f)
ha : p a
⊢ ↑(↑f { val := a, property := ha }) = ↑{ val := a, property := ha }
[PROOFSTEP]
simp_rw [mem_fixedPoints, IsFixedPt, Perm.subtypeEquivSubtypePerm, Equiv.coe_fn_mk, Perm.ofSubtype_apply_of_mem _ ha] at
  hfa
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
ha : p a
hfa : ↑(↑f { val := a, property := ha }) = a
⊢ ↑(↑f { val := a, property := ha }) = ↑{ val := a, property := ha }
[PROOFSTEP]
assumption
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
⊢ (∀ (a : α), a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f) → ¬p a) → f ∈ derangements (Subtype p)
[PROOFSTEP]
rintro hf ⟨a, ha⟩ hfa
[GOAL]
case refine'_2.mk
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ (a : α), a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f) → ¬p a
a : α
ha : p a
hfa : ↑f { val := a, property := ha } = { val := a, property := ha }
⊢ False
[PROOFSTEP]
refine' hf _ _ ha
[GOAL]
case refine'_2.mk
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ (a : α), a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f) → ¬p a
a : α
ha : p a
hfa : ↑f { val := a, property := ha } = { val := a, property := ha }
⊢ a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f)
[PROOFSTEP]
simp only [Perm.subtypeEquivSubtypePerm_apply_coe, mem_fixedPoints]
[GOAL]
case refine'_2.mk
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ (a : α), a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f) → ¬p a
a : α
ha : p a
hfa : ↑f { val := a, property := ha } = { val := a, property := ha }
⊢ IsFixedPt (↑(↑Perm.ofSubtype f)) a
[PROOFSTEP]
dsimp [IsFixedPt]
[GOAL]
case refine'_2.mk
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ (a : α), a ∈ fixedPoints ↑↑(↑(Perm.subtypeEquivSubtypePerm p) f) → ¬p a
a : α
ha : p a
hfa : ↑f { val := a, property := ha } = { val := a, property := ha }
⊢ ↑(↑Perm.ofSubtype f) a = a
[PROOFSTEP]
simp_rw [Perm.ofSubtype_apply_of_mem _ ha, hfa]
[GOAL]
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
⊢ (∃ _h, ∀ (a : α), a ∈ fixedPoints ↑f → ¬p a) ↔ ∀ (a : α), ¬p a ↔ a ∈ fixedPoints ↑f
[PROOFSTEP]
simp_rw [exists_prop, ← forall_and, ← iff_iff_implies_and_implies]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // a ∈ fixedPoints ↑↑f } ⊕ { f // ¬a ∈ fixedPoints ↑↑f } ≃
    { f // fixedPoints ↑f ⊆ {a} ∧ a ∈ fixedPoints ↑f } ⊕ { f // fixedPoints ↑f ⊆ {a} ∧ ¬a ∈ fixedPoints ↑f }
[PROOFSTEP]
refine' Equiv.sumCongr _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // a ∈ fixedPoints ↑↑f } ≃ { f // fixedPoints ↑f ⊆ {a} ∧ a ∈ fixedPoints ↑f }
[PROOFSTEP]
exact subtypeSubtypeEquivSubtypeInter (fun x : Perm α => fixedPoints x ⊆ { a }) (a ∈ fixedPoints ·)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // ¬a ∈ fixedPoints ↑↑f } ≃ { f // fixedPoints ↑f ⊆ {a} ∧ ¬a ∈ fixedPoints ↑f }
[PROOFSTEP]
exact subtypeSubtypeEquivSubtypeInter (fun x : Perm α => fixedPoints x ⊆ { a }) (¬a ∈ fixedPoints ·)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // fixedPoints ↑f ⊆ {a} ∧ a ∈ fixedPoints ↑f } ⊕ { f // fixedPoints ↑f ⊆ {a} ∧ ¬a ∈ fixedPoints ↑f } ≃
    { f // fixedPoints ↑f = {a} } ⊕ { f // fixedPoints ↑f = ∅ }
[PROOFSTEP]
refine' Equiv.sumCongr (subtypeEquivRight fun f => _) (subtypeEquivRight fun f => _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ↑f ⊆ {a} ∧ a ∈ fixedPoints ↑f ↔ fixedPoints ↑f = {a}
[PROOFSTEP]
rw [Set.eq_singleton_iff_unique_mem, and_comm]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ a ∈ fixedPoints ↑f ∧ fixedPoints ↑f ⊆ {a} ↔ a ∈ fixedPoints ↑f ∧ ∀ (x : α), x ∈ fixedPoints ↑f → x = a
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ↑f ⊆ {a} ∧ ¬a ∈ fixedPoints ↑f ↔ fixedPoints ↑f = ∅
[PROOFSTEP]
rw [Set.eq_empty_iff_forall_not_mem]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ↑f ⊆ {a} ∧ ¬a ∈ fixedPoints ↑f ↔ ∀ (x : α), ¬x ∈ fixedPoints ↑f
[PROOFSTEP]
refine' ⟨fun h x hx => h.2 (h.1 hx ▸ hx), fun h => ⟨fun x hx => (h _ hx).elim, h _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // fixedPoints ↑f = {a} } ⊕ { f // fixedPoints ↑f = ∅ } ≃ ↑(derangements ↑{a}ᶜ) ⊕ ↑(derangements α)
[PROOFSTEP]
refine'
  Equiv.sumCongr ((derangements.subtypeEquiv (· ∈ ({ a }ᶜ : Set α))).trans <| subtypeEquivRight fun x => _).symm
    (subtypeEquivRight fun f => mem_derangements_iff_fixedPoints_eq_empty.symm)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), ¬a_1 ∈ {a}ᶜ ↔ a_1 ∈ fixedPoints ↑x) ↔ fixedPoints ↑x = {a}
[PROOFSTEP]
rw [eq_comm, Set.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), ¬a_1 ∈ {a}ᶜ ↔ a_1 ∈ fixedPoints ↑x) ↔ ∀ (x_1 : α), x_1 ∈ {a} ↔ x_1 ∈ fixedPoints ↑x
[PROOFSTEP]
simp_rw [Set.mem_compl_iff, Classical.not_not]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : Option α
f : Perm α
⊢ f ∈ fiber a ↔ ∃ F, F ∈ derangements (Option α) ∧ ↑F none = a ∧ removeNone F = f
[PROOFSTEP]
simp [RemoveNone.fiber, derangements]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ fiber none = ∅
[PROOFSTEP]
rw [Set.eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ∀ (x : Perm α), ¬x ∈ fiber none
[PROOFSTEP]
intro f hyp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
f : Perm α
hyp : f ∈ fiber none
⊢ False
[PROOFSTEP]
rw [RemoveNone.mem_fiber] at hyp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
f : Perm α
hyp : ∃ F, F ∈ derangements (Option α) ∧ ↑F none = none ∧ removeNone F = f
⊢ False
[PROOFSTEP]
rcases hyp with ⟨F, F_derangement, F_none, _⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
f : Perm α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = none
right✝ : removeNone F = f
⊢ False
[PROOFSTEP]
exact F_derangement none F_none
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ fiber (some a) = {f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
ext f
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) ↔ f ∈ {f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) → f ∈ {f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
rw [RemoveNone.mem_fiber]
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ (∃ F, F ∈ derangements (Option α) ∧ ↑F none = some a ∧ removeNone F = f) → f ∈ {f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
rintro ⟨F, F_derangement, F_none, rfl⟩ x x_fixed
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : x ∈ fixedPoints ↑(removeNone F)
⊢ x ∈ {a}
[PROOFSTEP]
rw [mem_fixedPoints_iff] at x_fixed
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : ↑(removeNone F) x = x
⊢ x ∈ {a}
[PROOFSTEP]
apply_fun some at x_fixed
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : some (↑(removeNone F) x) = some x
⊢ x ∈ {a}
[PROOFSTEP]
cases' Fx : F (some x) with y
[GOAL]
case h.mp.intro.intro.intro.none
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : some (↑(removeNone F) x) = some x
Fx : ↑F (some x) = none
⊢ x ∈ {a}
[PROOFSTEP]
rwa [removeNone_none F Fx, F_none, Option.some_inj, eq_comm] at x_fixed
[GOAL]
case h.mp.intro.intro.intro.some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : some (↑(removeNone F) x) = some x
y : α
Fx : ↑F (some x) = some y
⊢ x ∈ {a}
[PROOFSTEP]
exfalso
[GOAL]
case h.mp.intro.intro.intro.some.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : some (↑(removeNone F) x) = some x
y : α
Fx : ↑F (some x) = some y
⊢ False
[PROOFSTEP]
rw [removeNone_some F ⟨y, Fx⟩] at x_fixed
[GOAL]
case h.mp.intro.intro.intro.some.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : ↑F none = some a
x : α
x_fixed : ↑F (some x) = some x
y : α
Fx : ↑F (some x) = some y
⊢ False
[PROOFSTEP]
exact F_derangement _ x_fixed
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ {f | fixedPoints ↑f ⊆ {a}} → f ∈ fiber (some a)
[PROOFSTEP]
intro h_opfp
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ f ∈ fiber (some a)
[PROOFSTEP]
use Equiv.Perm.decomposeOption.symm (some a, f)
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑Perm.decomposeOption.symm (some a, f) ∈ derangements (Option α) ∧
    ↑Perm.decomposeOption (↑Perm.decomposeOption.symm (some a, f)) = (some a, f)
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑Perm.decomposeOption.symm (some a, f) ∈ derangements (Option α)
[PROOFSTEP]
intro x
[GOAL]
case h.left
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : Option α
⊢ ↑(↑Perm.decomposeOption.symm (some a, f)) x ≠ x
[PROOFSTEP]
apply_fun fun x => Equiv.swap none (some a) x
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : Option α
⊢ (fun x => ↑(Equiv.swap none (some a)) x) (↑(↑Perm.decomposeOption.symm (some a, f)) x) ≠
    (fun x => ↑(Equiv.swap none (some a)) x) x
[PROOFSTEP]
simp only [Perm.decomposeOption_symm_apply, swap_apply_self, Perm.coe_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : Option α
⊢ ↑(Equiv.swap none (some a)) ((↑(Equiv.swap none (some a)) ∘ ↑(optionCongr f)) x) ≠ ↑(Equiv.swap none (some a)) x
[PROOFSTEP]
cases' x with x
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑(Equiv.swap none (some a)) ((↑(Equiv.swap none (some a)) ∘ ↑(optionCongr f)) none) ≠ ↑(Equiv.swap none (some a)) none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
⊢ ↑(Equiv.swap none (some a)) ((↑(Equiv.swap none (some a)) ∘ ↑(optionCongr f)) (some x)) ≠
    ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
simp only [comp, optionCongr_apply, Option.map_some', swap_apply_self]
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
by_cases x_vs_a : x = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
rw [x_vs_a, swap_apply_right]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (↑f a) ≠ none
[PROOFSTEP]
apply Option.some_ne_none
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
have ne_1 : some x ≠ none := Option.some_ne_none _
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
have ne_2 : some x ≠ some a := (Option.some_injective α).ne_iff.mpr x_vs_a
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ some (↑f x) ≠ ↑(Equiv.swap none (some a)) (some x)
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne ne_1 ne_2, (Option.some_injective α).ne_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ ↑f x ≠ x
[PROOFSTEP]
intro contra
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
contra : ↑f x = x
⊢ False
[PROOFSTEP]
exact x_vs_a (h_opfp contra)
[GOAL]
case h.right
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ↑f ⊆ {a}}
⊢ ↑Perm.decomposeOption (↑Perm.decomposeOption.symm (some a, f)) = (some a, f)
[PROOFSTEP]
rw [apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ↑(derangements (Option α)) ≃ (a : α) × ↑{f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
have fiber_none_is_false : Equiv.RemoveNone.fiber (@none α) → False :=
  by
  rw [Equiv.RemoveNone.fiber_none]
  exact IsEmpty.false
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ↑(Equiv.RemoveNone.fiber none) → False
[PROOFSTEP]
rw [Equiv.RemoveNone.fiber_none]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
⊢ ↑∅ → False
[PROOFSTEP]
exact IsEmpty.false
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ↑(Equiv.RemoveNone.fiber none) → False
⊢ ↑(derangements (Option α)) ≃ (a : α) × ↑{f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
calc
  derangements (Option α) ≃ Equiv.Perm.decomposeOption '' derangements (Option α) := Equiv.image _ _
  _ ≃ Σ a : Option α, ↥(Equiv.RemoveNone.fiber a) := (setProdEquivSigma _)
  _ ≃ Σ a : α, ↥(Equiv.RemoveNone.fiber (some a)) := (sigmaOptionEquivOfSome _ fiber_none_is_false)
  _ ≃ Σ a : α, {f : Perm α | fixedPoints f ⊆ { a }} :=
    by
    simp_rw [Equiv.RemoveNone.fiber_some]
    rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ↑(Equiv.RemoveNone.fiber none) → False
⊢ (a : α) × ↑(Equiv.RemoveNone.fiber (some a)) ≃ (a : α) × ↑{f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
simp_rw [Equiv.RemoveNone.fiber_some]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ↑(Equiv.RemoveNone.fiber none) → False
⊢ (a : α) × ↑{f | fixedPoints ↑f ⊆ {a}} ≃ (a : α) × ↑{f | fixedPoints ↑f ⊆ {a}}
[PROOFSTEP]
rfl