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

Goal state before:
pp: case inr
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s) x

Tactic:
simp_rw [setToSimpleFunc]

Goal state after:
case inr
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
⊢ ∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
      (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    (T s) x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case inr.inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet Set.univ
hs_empty : Set.univ.Nonempty
⊢ ∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range,
      (T (⇑(piecewise Set.univ hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    (T Set.univ) x

pp: case inr.inr
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
⊢ ∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
      (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    (T s) x

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet Set.univ
hs_empty : Set.univ.Nonempty
⊢ ∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range,
      (T (⇑(piecewise Set.univ hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    (T Set.univ) x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case pos
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : x = 0
⊢ ∑ x_1 ∈ {x, 0}, (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T s) x

pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ ∑ x_1 ∈ {x, 0}, (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T s) x

Tactic:
·

Goal state after:
case pos
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : x = 0
⊢ ∑ x_1 ∈ {x, 0}, (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 = (T s) x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ x ∉ {0}

pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x})) x +
      ∑ x_1 ∈ {0}, (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    (T s) x

Tactic:
·

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ x ∉ {0}
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
⊢ ∀ ⦃f g : α →ₛ E⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (MemLp (⇑f) p μ → motive ⇑f) → (MemLp (⇑g) p μ → motive ⇑g) → MemLp (⇑(f + g)) p μ → motive ⇑(f + g)

Tactic:
·

Goal state after:
case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
⊢ ∀ ⦃f g : α →ₛ E⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (MemLp (⇑f) p μ → motive ⇑f) → (MemLp (⇑g) p μ → motive ⇑g) → MemLp (⇑(f + g)) p μ → motive ⇑(f + g)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ x ∈ {x}

pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.ite Set.univ (0 ⁻¹' {x}) = s

Tactic:
·

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ x ∈ {x}
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ 0 ∉ {x}

pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.ite Set.univ ∅ = s

Tactic:
·

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ 0 ∉ {x}
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
⊢ setToSimpleFunc T (const α x) = (T Set.univ) x

pp: case inr
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h✝ : Nonempty α
⊢ setToSimpleFunc T (const α x) = (T Set.univ) x

Tactic:
·

Goal state after:
case inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
⊢ setToSimpleFunc T (const α x) = (T Set.univ) x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case inr
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h✝ : Nonempty α
⊢ setToSimpleFunc T (const α x) = (T Set.univ) x

Tactic:
·

Goal state after:
case inr
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h✝ : Nonempty α
⊢ setToSimpleFunc T (const α x) = (T Set.univ) x
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x ↦ c) l (𝓝 0)
⊢ Tendsto u l (𝓝 c)

pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
⊢ Tendsto (u - fun x ↦ c) l (𝓝 0)

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x ↦ c) l (𝓝 0)
⊢ Tendsto u l (𝓝 c)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
⊢ Tendsto (u - fun x ↦ c) l (𝓝 0)

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
⊢ Tendsto (u - fun x ↦ c) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
hu : u ~[l] const α 0
⊢ Tendsto u l (𝓝 0)

pp: case inr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
h : ¬c = 0
⊢ Tendsto u l (𝓝 c)

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
hu : u ~[l] const α 0
⊢ Tendsto u l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
h : ¬c = 0
⊢ Tendsto u l (𝓝 c)

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
h : ¬c = 0
⊢ Tendsto u l (𝓝 c)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : c = 0
⊢ Tendsto v l (𝓝 c)

pp: case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
⊢ Tendsto v l (𝓝 c)

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : c = 0
⊢ Tendsto v l (𝓝 c)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
⊢ Tendsto v l (𝓝 c)

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
⊢ Tendsto v l (𝓝 c)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬Integrable f μ
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
·

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ (fun a ↦ ENNReal.ofReal (-f a)) =ᵐ[μ] 0

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ AEMeasurable (fun a ↦ ENNReal.ofReal (-f a)) μ

Tactic:
·

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ (fun a ↦ ENNReal.ofReal (-f a)) =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ AEMeasurable (fun a ↦ ENNReal.ofReal (-f a)) μ

Tactic:
·

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ AEMeasurable (fun a ↦ ENNReal.ofReal (-f a)) μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬Integrable f μ
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
·

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬Integrable f μ
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mp.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ Tendsto (φ + 1) l (𝓝 1)

pp: case mp.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ u =ᶠ[l] (φ + 1) * v

pp: case mpr.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 0)

pp: case mpr.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v

Tactic:
·

Goal state after:
case mp.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ Tendsto (φ + 1) l (𝓝 1)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mp.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ u =ᶠ[l] (φ + 1) * v

pp: case mpr.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 0)

pp: case mpr.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v

Tactic:
·

Goal state after:
case mp.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ u =ᶠ[l] (φ + 1) * v
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mpr.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 0)

pp: case mpr.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v

Tactic:
·

Goal state after:
case mpr.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mpr.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v

Tactic:
·

Goal state after:
case mpr.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ 0 ≤ᵐ[μ] fun x ↦ ‖f x‖

Tactic:
·

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ 0 ≤ᵐ[μ] fun x ↦ ‖f x‖

Tactic:
·

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ 0 ≤ᵐ[μ] fun x ↦ ‖f x‖
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ u ~[l] v → Tendsto (u / v) l (𝓝 1)

pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ Tendsto (u / v) l (𝓝 1) → u ~[l] v

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ u ~[l] v → Tendsto (u / v) l (𝓝 1)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
x✝ : α
⊢ (u / v) x✝ = u x✝ / v x✝ - v x✝ / v x✝ + v x✝ / v x✝

pp: case e'_5
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
⊢ 1 = 0 + 1

Tactic:
·

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
x✝ : α
⊢ (u / v) x✝ = u x✝ / v x✝ - v x✝ / v x✝ + v x✝ / v x✝
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
⊢ 1 = 0 + 1

Tactic:
·

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x ↦ v x / v x) l (𝓝 1)
⊢ 1 = 0 + 1
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ Tendsto (u / v) l (𝓝 1) → u ~[l] v

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ Tendsto (u / v) l (𝓝 1) → u ~[l] v
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ (∫⁻ (x : α), ‖(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖ₑ ∂μ).toReal =
    (ENNReal.toReal ∘ fun n ↦ ∫⁻ (x : α), ‖(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖ₑ ∂μ) n

pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ AEStronglyMeasurable (fun x ↦ (approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x) μ

Tactic:
·

Goal state after:
case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ (∫⁻ (x : α), ‖(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖ₑ ∂μ).toReal =
    (ENNReal.toReal ∘ fun n ↦ ∫⁻ (x : α), ‖(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖ₑ ∂μ) n
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ AEStronglyMeasurable (fun x ↦ (approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x) μ

Tactic:
·

Goal state after:
case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
n : ℕ
⊢ AEStronglyMeasurable (fun x ↦ (approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x) μ