α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
⊢ (∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
simp_rw [← iSup_apply]
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
let p : α → (ℕ → ℝ≥0∞) → Prop := fun _ f' => Monotone f'
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have hp : ∀ᵐ x ∂μ, p x fun i => f i x := h_mono
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ (∫⁻ (a : α), iSup (fun n => aeSeq hf (fun x => p x) n) a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
rw [lintegral_congr_ae (aeSeq.iSup hf hp).symm]
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ (∫⁻ (a : α), ⨆ (i : ℕ), aeSeq hf (fun x f' => Monotone f') i a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ (∫⁻ (a : α), iSup (fun n => aeSeq hf (fun x => p x) n) a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
simp_rw [iSup_apply]
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), aeSeq hf p n a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ (∫⁻ (a : α), ⨆ (i : ℕ), aeSeq hf (fun x f' => Monotone f') i a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
rw [@lintegral_iSup _ _ μ _ (aeSeq.measurable hf p) h_ae_seq_mono]
case e_s
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ (fun n => ∫⁻ (a : α), aeSeq hf p n a ∂μ) = fun n => ∫⁻ (a : α), f n a ∂μ
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ (⨆ (n : ℕ), ∫⁻ (a : α), aeSeq hf p n a ∂μ) = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
congr
no goals
case e_s
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ (fun n => ∫⁻ (a : α), aeSeq hf p n a ∂μ) = fun n => ∫⁻ (a : α), f n a ∂μ
exact funext fun n => lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae hf hp n)
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
⊢ aeSeq hf p n x ≤ aeSeq hf p m x
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
⊢ Monotone (aeSeq hf p)
intro n m hnm x
case pos
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p n x ≤ aeSeq hf p m x

case neg
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : ¬x ∈ aeSeqSet hf p
⊢ aeSeq hf p n x ≤ aeSeq hf p m x
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
⊢ aeSeq hf p n x ≤ aeSeq hf p m x
by_cases hx : x ∈ aeSeqSet hf p
no goals
case pos
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p n x ≤ aeSeq hf p m x
exact aeSeq.prop_of_mem_aeSeqSet hf hx hnm
case neg
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : ¬x ∈ aeSeqSet hf p
⊢ Nonempty.some (_ : Nonempty ℝ≥0∞) ≤ Nonempty.some (_ : Nonempty ℝ≥0∞)
case neg
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : ¬x ∈ aeSeqSet hf p
⊢ aeSeq hf p n x ≤ aeSeq hf p m x
simp only [aeSeq, hx, if_false]
no goals
case neg
α : Type u_1
β : Type ?u.480111
γ : Type ?u.480114
δ : Type ?u.480117
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n)
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : ¬x ∈ aeSeqSet hf p
⊢ Nonempty.some (_ : Nonempty ℝ≥0∞) ≤ Nonempty.some (_ : Nonempty ℝ≥0∞)
exact le_rfl