case zero
α : Type u_1
β : Type ?u.104521
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.zero), f k x) ∈ measurableLE μ ν

case succ
α : Type u_1
β : Type ?u.104521
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ (k : ℕ) (_ : k ≤ m), f k x) ∈ measurableLE μ ν
⊢ (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.succ m), f k x) ∈ measurableLE μ ν
α : Type u_1
β : Type ?u.104521
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
⊢ (fun x => ⨆ (k : ℕ) (_ : k ≤ n), f k x) ∈ measurableLE μ ν
induction' n with m hm
case zero.refine'_1
α : Type u_1
β : Type ?u.104521
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ Measurable fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.zero), f k x

case zero.refine'_2
α : Type u_1
β : Type ?u.104521
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ ∀ (A : Set α), MeasurableSet A → (∫⁻ (x : α) in A, (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.zero), f k x) x ∂μ) ≤ ↑↑ν A
case zero
α : Type u_1
β : Type ?u.104521
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.zero), f k x) ∈ measurableLE μ ν
refine' ⟨_, _⟩
no goals
case zero.refine'_1
α : Type u_1
β : Type ?u.104521
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ Measurable fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.zero), f k x
simp [(hf 0).1]
case zero.refine'_2
α : Type u_1
β : Type ?u.104521
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (x : α) in A, (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.zero), f k x) x ∂μ) ≤ ↑↑ν A
case zero.refine'_2
α : Type u_1
β : Type ?u.104521
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ ∀ (A : Set α), MeasurableSet A → (∫⁻ (x : α) in A, (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.zero), f k x) x ∂μ) ≤ ↑↑ν A
intro A hA
no goals
case zero.refine'_2
α : Type u_1
β : Type ?u.104521
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (x : α) in A, (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.zero), f k x) x ∂μ) ≤ ↑↑ν A
simp [(hf 0).2 A hA]
case succ
α : Type u_1
β : Type ?u.104521
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ (k : ℕ) (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a => f (Nat.succ m) a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a
⊢ (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.succ m), f k x) ∈ measurableLE μ ν
case succ
α : Type u_1
β : Type ?u.104521
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ (k : ℕ) (_ : k ≤ m), f k x) ∈ measurableLE μ ν
⊢ (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.succ m), f k x) ∈ measurableLE μ ν
have :
  (fun a : α => ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a =>
    f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a :=
  funext fun _ => iSup_succ_eq_sup _ _ _
case succ
α : Type u_1
β : Type ?u.104521
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ (k : ℕ) (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a => f (Nat.succ m) a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (x : α) in A, (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.succ m), f k x) x ∂μ) ≤ ↑↑ν A
case succ
α : Type u_1
β : Type ?u.104521
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ (k : ℕ) (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a => f (Nat.succ m) a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a
⊢ (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.succ m), f k x) ∈ measurableLE μ ν
refine' ⟨measurable_iSup fun n => Measurable.iSup_Prop _ (hf n).1, fun A hA => _⟩
case succ
α : Type u_1
β : Type ?u.104521
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ (k : ℕ) (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a => f (Nat.succ m) a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A, f (Nat.succ m) a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a ∂μ) ≤ ↑↑ν A
case succ
α : Type u_1
β : Type ?u.104521
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ (k : ℕ) (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a => f (Nat.succ m) a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (x : α) in A, (fun x => ⨆ (k : ℕ) (_ : k ≤ Nat.succ m), f k x) x ∂μ) ≤ ↑↑ν A
rw [this]
no goals
case succ
α : Type u_1
β : Type ?u.104521
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun x => ⨆ (k : ℕ) (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this : (fun a => ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a => f (Nat.succ m) a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (a : α) in A, f (Nat.succ m) a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a ∂μ) ≤ ↑↑ν A
exact (sup_mem_measurableLE (hf m.succ) hm).2 A hA