mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet h_meas p
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet h_meas p
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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

Tactic:
aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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 ≤ aeSeq hf p z x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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 ≤ aeSeq hf p z x

Tactic:
aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
h : x ∈ s
⊢ f x = f x

pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
h : x ∉ s
⊢ f x = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
h : x ∈ s
⊢ f x = f x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
h : x ∉ s
⊢ f x = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
h : x ∉ s
⊢ f x = 0
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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

Tactic:
aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ x ∈ {x | f x = r}, f x = r
⊢ ∫⁻ (x : α) in {x | f x = r}, r ∂μ = r * μ {x | f x = r}

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ x ∈ {x | f x = r}, f x = r
⊢ MeasurableSet {x | f x = r}

Tactic:
·

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ x ∈ {x | f x = r}, f x = r
⊢ ∫⁻ (x : α) in {x | f x = r}, r ∂μ = r * μ {x | f x = r}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ⨅ n, ∫⁻ (a : α), aeSeq h_meas p n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), aeSeq h_meas p 0 a ∂μ ≠ ∞

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ⨅ n, ∫⁻ (a : α), aeSeq h_meas p n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ x ∈ {x | f x = r}, f x = r
⊢ MeasurableSet {x | f x = r}

Tactic:
·

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ x ∈ {x | f x = r}, f x = r
⊢ MeasurableSet {x | f x = r}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), aeSeq h_meas p 0 a ∂μ ≠ ∞

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), aeSeq h_meas p 0 a ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | f x ≠ 0}
h : f x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ ((hf.approx n).restrict {x | f x ≠ 0})⁻¹) n) x) atTop (𝓝 (f⁻¹ x))

pp: case neg
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | f x ≠ 0}
h : ¬f x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ ((hf.approx n).restrict {x | f x ≠ 0})⁻¹) n) x) atTop (𝓝 (f⁻¹ x))

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | f x ≠ 0}
h : f x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ ((hf.approx n).restrict {x | f x ≠ 0})⁻¹) n) x) atTop (𝓝 (f⁻¹ x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: case intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : IsEmpty β
⊢ ∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ

pp: case intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
⊢ ∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
·

Goal state after:
case intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : IsEmpty β
⊢ ∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case e'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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 : α), (⨆ i, f i) a ∂μ = ∫⁻ (a : α), ⨆ b, aeSeq hf p b a ∂?m.244

pp: case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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.244

pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := ⋯
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ Measure α

Tactic:
·

Goal state after:
case e'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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 : α), (⨆ i, f i) a ∂μ = ∫⁻ (a : α), ⨆ b, aeSeq hf p b a ∂?m.244
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | f x ≠ 0}
h : ¬f x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ ((hf.approx n).restrict {x | f x ≠ 0})⁻¹) n) x) atTop (𝓝 (f⁻¹ x))

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | f x ≠ 0}
h : ¬f x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ ((hf.approx n).restrict {x | f x ≠ 0})⁻¹) n) x) atTop (𝓝 (f⁻¹ x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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 ∂μ

Tactic:
·

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) 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 ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
⊢ ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) 0 a ∂μ ≠ ∞

pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
⊢ ∀ (n : ℕ), Measurable ((f ∘ Directed.sequence f h_directed) n)

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
⊢ ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) 0 a ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
⊢ ∀ (n : ℕ), Measurable ((f ∘ Directed.sequence f h_directed) n)

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
⊢ ∀ (n : ℕ), Measurable ((f ∘ Directed.sequence f h_directed) n)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : ¬u.NeBot
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u

pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
·

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : ¬u.NeBot
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | g x ≠ 0}
h : g x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}) n) x) atTop (𝓝 ((f / g) x))

pp: case neg
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | g x ≠ 0}
h : ¬g x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}) n) x) atTop (𝓝 ((f / g) x))

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | g x ≠ 0}
h : g x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}) n) x) atTop (𝓝 ((f / g) x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
·

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
b : β
⊢ ⨅ n, ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ ≤ ∫⁻ (a : α), f b a ∂μ

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
n : ℕ
⊢ ⨅ b, ∫⁻ (a : α), f b a ∂μ ≤ ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
b : β
⊢ ⨅ n, ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ ≤ ∫⁻ (a : α), f b a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
n : ℕ
⊢ ⨅ b, ∫⁻ (a : α), f b a ∂μ ≤ ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
n : ℕ
⊢ ⨅ b, ∫⁻ (a : α), f b a ∂μ ≤ ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable ⇑(eapprox f n)

pp: case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n ↦ ⇑(eapprox f n)

Tactic:
·

Goal state after:
case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable ⇑(eapprox f n)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | g x ≠ 0}
h : ¬g x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}) n) x) atTop (𝓝 ((f / g) x))

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | g x ≠ 0}
h : ¬g x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}) n) x) atTop (𝓝 ((f / g) x))