α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
⊢ Tendsto (fun i => ∫ (a : α) in s i, f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
⊢ Tendsto (fun i => ∫ (a : α) in s i, f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
let bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ Tendsto (fun i => ∫ (a : α) in s i, f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
⊢ Tendsto (fun i => ∫ (a : α) in s i, f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
have h_int_eq : (fun i => ∫ a in s i, f a ∂μ) = fun i => ∫ a, (s i).indicator f a ∂μ :=
  funext fun i => (integral_indicator (hsm i)).symm
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ Tendsto (fun i => ∫ (a : α), indicator (s i) f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ Tendsto (fun i => ∫ (a : α) in s i, f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
rw [h_int_eq]
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ Tendsto (fun i => ∫ (a : α), indicator (s i) f a ∂μ) atTop
    (𝓝 (∫ (x : α), indicator (⋂ (b : ℕ), s b) (fun a => f a) x ∂μ))
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ Tendsto (fun i => ∫ (a : α), indicator (s i) f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
rw [← integral_indicator (MeasurableSet.iInter hsm)]
case refine'_1
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ ∀ (n : ℕ), AEStronglyMeasurable (fun a => indicator (s n) f a) μ

case refine'_2
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ Integrable bound

case refine'_3
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖indicator (s n) f a‖ ≤ bound a

case refine'_4
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => indicator (s n) f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) (fun a => f a) a))
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ Tendsto (fun i => ∫ (a : α), indicator (s i) f a ∂μ) atTop
    (𝓝 (∫ (x : α), indicator (⋂ (b : ℕ), s b) (fun a => f a) x ∂μ))
refine' tendsto_integral_of_dominated_convergence bound _ _ _ _
case refine'_1
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
n : ℕ
⊢ AEStronglyMeasurable (fun a => indicator (s n) f a) μ
case refine'_1
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ ∀ (n : ℕ), AEStronglyMeasurable (fun a => indicator (s n) f a) μ
intro n
case refine'_1
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
n : ℕ
⊢ AEStronglyMeasurable f (Measure.restrict μ (s n))
case refine'_1
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
n : ℕ
⊢ AEStronglyMeasurable (fun a => indicator (s n) f a) μ
rw [aestronglyMeasurable_indicator_iff (hsm n)]
no goals
case refine'_1
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
n : ℕ
⊢ AEStronglyMeasurable f (Measure.restrict μ (s n))
exact (IntegrableOn.mono_set hfi (h_anti (zero_le n))).1
case refine'_2
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ IntegrableOn (fun a => ‖f a‖) (s 0)
case refine'_2
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ Integrable bound
rw [integrable_indicator_iff (hsm 0)]
no goals
case refine'_2
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ IntegrableOn (fun a => ‖f a‖) (s 0)
exact hfi.norm
case refine'_3
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, indicator (s n) (fun a => ‖f a‖) a ≤ indicator (s 0) (fun a => ‖f a‖) a
case refine'_3
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖indicator (s n) f a‖ ≤ bound a
simp_rw [norm_indicator_eq_indicator_norm]
case refine'_3
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
n : ℕ
x : α
⊢ indicator (s n) (fun a => ‖f a‖) x ≤ indicator (s 0) (fun a => ‖f a‖) x
case refine'_3
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, indicator (s n) (fun a => ‖f a‖) a ≤ indicator (s 0) (fun a => ‖f a‖) a
refine' fun n => eventually_of_forall fun x => _
no goals
case refine'_3
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
n : ℕ
x : α
⊢ indicator (s n) (fun a => ‖f a‖) x ≤ indicator (s 0) (fun a => ‖f a‖) x
exact indicator_le_indicator_of_subset (h_anti (zero_le n)) (fun a => norm_nonneg _) _
no goals
case refine'_4
α : Type u_1
β : Type ?u.314392
E : Type u_2
F : Type ?u.314398
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0)
bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), indicator (s i) f a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => indicator (s n) f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) (fun a => f a) a))
filter_upwards [] with a using le_trans (h_anti.tendsto_indicator _ _ _) (pure_le_nhds _)