α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
⊢ (∫⁻ (a : α), ⨆ (b : β), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
simp_rw [← iSup_apply]
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
let p : α → (β → ENNReal) → Prop := fun x f' => Directed LE.le f'
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have hp : ∀ᵐ x ∂μ, p x fun i => f i x := by
  filter_upwards [] with x i j
  obtain ⟨z, hz₁, hz₂⟩ := h_directed i j
  exact ⟨z, hz₁ x, hz₂ x⟩
case h.e'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ∫⁻ (a : α), ⨆ (b : β), aeSeq hf p b a ∂?m.1013517

case h.e'_3
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ (⨆ (b : β), ∫⁻ (a : α), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), aeSeq hf p b a ∂?m.1013517

α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ Measure α
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
convert lintegral_iSup_directed_of_measurable (aeSeq.measurable hf p) h_ae_seq_directed using 1
case h
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
x : α
i j : β
⊢ ∃ z, (fun i => f i x) i ≤ (fun i => f i x) z ∧ (fun i => f i x) j ≤ (fun i => f i x) z
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
⊢ ∀ᵐ (x : α) ∂μ, p x fun i => f i x
filter_upwards [] with x i j
case h.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
x : α
i j z : β
hz₁ : f i ≤ f z
hz₂ : f j ≤ f z
⊢ ∃ z, (fun i => f i x) i ≤ (fun i => f i x) z ∧ (fun i => f i x) j ≤ (fun i => f i x) z
case h
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
x : α
i j : β
⊢ ∃ z, (fun i => f i x) i ≤ (fun i => f i x) z ∧ (fun i => f i x) j ≤ (fun i => f i x) z
obtain ⟨z, hz₁, hz₂⟩ := h_directed i j
no goals
case h.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
x : α
i j z : β
hz₁ : f i ≤ f z
hz₂ : f j ≤ f z
⊢ ∃ z, (fun i => f i x) i ≤ (fun i => f i x) z ∧ (fun i => f i x) j ≤ (fun i => f i x) z
exact ⟨z, hz₁ x, hz₂ x⟩
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ : β
⊢ ∃ z, aeSeq hf p b₁ ≤ aeSeq hf p z ∧ aeSeq hf p b₂ ≤ aeSeq hf p z
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
⊢ Directed LE.le (aeSeq hf p)
intro b₁ b₂
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
⊢ ∃ z, aeSeq hf p b₁ ≤ aeSeq hf p z ∧ aeSeq hf p b₂ ≤ aeSeq hf p z
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ : β
⊢ ∃ z, aeSeq hf p b₁ ≤ aeSeq hf p z ∧ aeSeq hf p b₂ ≤ aeSeq hf p z
obtain ⟨z, hz₁, hz₂⟩ := h_directed b₁ b₂
case intro.intro.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x
case intro.intro.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
⊢ aeSeq hf p b₂ ≤ aeSeq hf p z
intro x
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x

case neg
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : ¬x ∈ aeSeqSet hf p
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x
case intro.intro.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x
by_cases hx : x ∈ aeSeqSet hf p
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ f b₂ x ≤ f z x
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x
repeat' rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
no goals
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ f b₂ x ≤ f z x
apply_rules [hz₁, hz₂]
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ f b₂ x ≤ f z x
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ f b₂ x ≤ f z x
rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : ¬x ∈ aeSeqSet hf p
⊢ Nonempty.some (_ : Nonempty ℝ≥0∞) ≤ Nonempty.some (_ : Nonempty ℝ≥0∞)
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : ¬x ∈ aeSeqSet hf p
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x
simp only [aeSeq, hx, if_false]
no goals
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : ¬x ∈ aeSeqSet hf p
⊢ Nonempty.some (_ : Nonempty ℝ≥0∞) ≤ Nonempty.some (_ : Nonempty ℝ≥0∞)
exact le_rfl
case h.e'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) =
    ∫⁻ (a : α), iSup (fun i => aeSeq hf (fun x f' => Directed LE.le f') i) a ∂?m.1013517
case h.e'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) = ∫⁻ (a : α), ⨆ (b : β), aeSeq hf p b a ∂?m.1013517
simp_rw [← iSup_apply]
no goals
case h.e'_2
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ (∫⁻ (a : α), iSup (fun i => f i) a ∂μ) =
    ∫⁻ (a : α), iSup (fun i => aeSeq hf (fun x f' => Directed LE.le f') i) a ∂?m.1013517
rw [lintegral_congr_ae (aeSeq.iSup hf hp).symm]
case h.e'_3.e_s
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ (fun b => ∫⁻ (a : α), f b a ∂μ) = fun b => ∫⁻ (a : α), aeSeq hf p b a ∂μ
case h.e'_3
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ (⨆ (b : β), ∫⁻ (a : α), f b a ∂μ) = ⨆ (b : β), ∫⁻ (a : α), aeSeq hf p b a ∂μ
congr 1
case h.e'_3.e_s.h
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ (∫⁻ (a : α), f b a ∂μ) = ∫⁻ (a : α), aeSeq hf p b a ∂μ
case h.e'_3.e_s
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ (fun b => ∫⁻ (a : α), f b a ∂μ) = fun b => ∫⁻ (a : α), aeSeq hf p b a ∂μ
ext1 b
case h.e'_3.e_s.h
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ (fun a => f b a) =ᵐ[μ] fun a => aeSeq hf p b a
case h.e'_3.e_s.h
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ (∫⁻ (a : α), f b a ∂μ) = ∫⁻ (a : α), aeSeq hf p b a ∂μ
rw [lintegral_congr_ae]
case h.e'_3.e_s.h.H
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ (fun a => aeSeq hf p b a) =ᵐ[μ] fun a => f b a
case h.e'_3.e_s.h
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ (fun a => f b a) =ᵐ[μ] fun a => aeSeq hf p b a
apply EventuallyEq.symm
no goals
case h.e'_3.e_s.h.H
α : Type u_2
β : Type u_1
γ : Type ?u.1010067
δ : Type ?u.1010070
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b)
h_directed : Directed (fun x x_1 => x ≤ x_1) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ (fun a => aeSeq hf p b a) =ᵐ[μ] fun a => f b a
refine' aeSeq.aeSeq_n_eq_fun_n_ae hf hp _