mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε

Tactic:
]

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
ω : Ω
hω : f ω = AEStronglyMeasurable.mk f hf ω
⊢ (B (AEStronglyMeasurable.mk f hf ω)) (g ω) = (B (AEStronglyMeasurable.mk f hf ω)) (g ω)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
a : Ω
ha : f a = AEStronglyMeasurable.mk f hf a
⊢ (B (AEStronglyMeasurable.mk f hf a)) (μ[g | m] a) = (B (AEStronglyMeasurable.mk f hf a)) (μ[g | m] a)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
h₁ : ∀ l < k, 0 ≤ s (s.restrictNonposSeq i l)
this : 0 ≤ ∑' (l : ℕ), s (⋃ (_ : l < k), s.restrictNonposSeq i l)
⊢ s i < ∑' (i_1 : ℕ), s (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
h₁ : ∀ l < k, 0 ≤ s (s.restrictNonposSeq i l)
this : 0 ≤ ∑' (l : ℕ), s (⋃ (_ : l < k), s.restrictNonposSeq i l)
⊢ s i < ∑' (i_1 : ℕ), s (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
⊢ r • j = r • j

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : 0 ≤ r
⊢ (r.toNNReal • j).posPart = (r.toNNReal • j).posPart

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : 0 ≤ r
⊢ (r.toNNReal • j).negPart = (r.toNNReal • j).negPart

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ ((-r).toNNReal • j).negPart = ((-r).toNNReal • j).negPart

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ ((-r).toNNReal • j).posPart = ((-r).toNNReal • j).posPart

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
⊢ 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
i : Set α
hi : MeasurableSet i
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
i : Set α
hi : MeasurableSet i
⊢ j.negPart.real i - j.posPart.real i = j.negPart.real i - j.posPart.real i

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
⊢ f x = f x

pp: case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
⊢ x ∉ {x | ‖f x‖ < M}

pp: case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
⊢ x ∈ {x | M ≤ ↑‖f x‖₊}

Tactic:
]

Goal state after:
case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
⊢ x ∉ {x | ‖f x‖ < M}

case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
⊢ x ∈ {x | M ≤ ↑‖f x‖₊}
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑r * j.posPart.real i - ↑r * j.negPart.real i = r • j.posPart.real i - r • j.negPart.real i

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑r * j.posPart.real i - ↑r * j.negPart.real i = r • j.posPart.real i - r • j.negPart.real i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → v j ≤ w j
hi : ¬MeasurableSet i
⊢ 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → v j ≤ w j
hi : ¬MeasurableSet i
⊢ v ≤[i] w

Tactic:
· rw [restrict_not_measurable v hi, restrict_not_measurable w hi]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ -w (j ∩ i) ≤ -v (j ∩ i)

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ -w (j ∩ i) ≤ -v (j ∩ i)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
⊢ 0 ≤ j.negPart.real A

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
⊢ 0 ≤ j.negPart.real A
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ (v.restrict i) j ≤ (w.restrict i) j

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ (v.restrict i) j ≤ (w.restrict i) j
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
⊢ a ⊆ ⋃ i, f i

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
⊢ a ⊆ ⋃ i, f i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
⊢ 0 A ≤ j.posPart.real A

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
⊢ 0 A ≤ j.posPart.real A
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case e'_4
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
h₁ : ∀ l < k, 0 ≤ s (s.restrictNonposSeq i l)
l : ℕ
h : l < k
x : α
⊢ x ∈ s.restrictNonposSeq i l → l < k

Tactic:
]

Goal state after:
case e'_4
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
h₁ : ∀ l < k, 0 ≤ s (s.restrictNonposSeq i l)
l : ℕ
h : l < k
x : α
⊢ x ∈ s.restrictNonposSeq i l → l < k
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s✝ s : SignedMeasure α
i : Set α := ⋯.choose
hi : MeasurableSet ⋯.choose ∧ 0 ≤[⋯.choose] s ∧ s ≤[⋯.chooseᶜ] 0
⊢ ↑(NNReal.mk (s (⋯.choose ∩ ⋯.chooseᶜ)) ⋯) = 0

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s✝ s : SignedMeasure α
i : Set α := ⋯.choose
hi : MeasurableSet ⋯.choose ∧ 0 ≤[⋯.choose] s ∧ s ≤[⋯.chooseᶜ] 0
⊢ ↑(NNReal.mk (s (⋯.choose ∩ ⋯.chooseᶜ)) ⋯) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s✝ s : SignedMeasure α
i : Set α := ⋯.choose
hi : MeasurableSet ⋯.choose ∧ 0 ≤[⋯.choose] s ∧ s ≤[⋯.chooseᶜ] 0
⊢ ↑(NNReal.mk (-s (⋯.chooseᶜ ∩ ⋯.chooseᶜᶜ)) ⋯) = 0

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s✝ s : SignedMeasure α
i : Set α := ⋯.choose
hi : MeasurableSet ⋯.choose ∧ 0 ≤[⋯.choose] s ∧ s ≤[⋯.chooseᶜ] 0
⊢ ↑(NNReal.mk (-s (⋯.chooseᶜ ∩ ⋯.chooseᶜᶜ)) ⋯) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ ∑' (i : ℕ), v (a ∩ disjointed f i) ≤ ∑' (i : ℕ), w (a ∩ disjointed f i)

pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)

pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ ∑' (i : ℕ), v (a ∩ disjointed f i) ≤ ∑' (i : ℕ), w (a ∩ disjointed f i)

α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)

α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
k : Set α
hk : MeasurableSet k
⊢ s (i ∩ k) - -s (iᶜ ∩ k) = s k

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
k : Set α
hk : MeasurableSet k
⊢ s (i ∩ k) - -s (iᶜ ∩ k) = s k
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
k : Set α
hk : MeasurableSet k
⊢ s k = s k

pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
k : Set α
hk : MeasurableSet k
⊢ Disjoint (i ∩ k) (iᶜ ∩ k)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
k : Set α
hk : MeasurableSet k
⊢ Disjoint (i ∩ k) (iᶜ ∩ k)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : s w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ s w = s w

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
⊢ f x = f x

pp: case neg.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
⊢ x ∈ {x | ‖f x‖ < M}

pp: case neg.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
⊢ x ∉ {x | M ≤ ↑‖f x‖₊}

Tactic:
]

Goal state after:
case neg.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
⊢ x ∈ {x | ‖f x‖ < M}

case neg.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
⊢ x ∉ {x | M ≤ ↑‖f x‖₊}