mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : TopologicalSpace M
N : Type u_4
inst✝⁶ : AddCommMonoid N
inst✝⁵ : TopologicalSpace N
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousConstSMul R N
v : VectorMeasure α M
f : M →ₗ[R] N
hf : Continuous[inst✝⁷, inst✝⁵] ⇑f
c : R
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ((c • v).mapRange f.toAddMonoidHom hf) i✝ = (c • v.mapRange f.toAddMonoidHom hf) i✝

Tactic:
;

Goal state after:
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : TopologicalSpace M
N : Type u_4
inst✝⁶ : AddCommMonoid N
inst✝⁵ : TopologicalSpace N
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousConstSMul R N
v : VectorMeasure α M
f : M →ₗ[R] N
hf : Continuous[inst✝⁷, inst✝⁵] ⇑f
c : R
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ((c • v).mapRange f.toAddMonoidHom hf) i✝ = (c • v.mapRange f.toAddMonoidHom hf) i✝
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.someExistsOneDivLT (i \ ∅) ⊆ i

Tactic:
;

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.someExistsOneDivLT (i \ ∅) ⊆ i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ s.someExistsOneDivLT
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n✝),
            have this := ⋯;
            s.restrictNonposSeq i k) ⊆
    i

Tactic:
;

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ s.someExistsOneDivLT
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n✝),
            have this := ⋯;
            s.restrictNonposSeq i k) ⊆
    i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
⊢ 0 < s (s.someExistsOneDivLT (i \ ∅))

Tactic:
;

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
⊢ 0 < s (s.someExistsOneDivLT (i \ ∅))
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (v.restrict univ) i = v i

Tactic:
rw [restrict_apply v MeasurableSet.univ hi, Set.inter_univ]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
h : n < 0
hx₂ : x ∈ s.restrictNonposSeq i 0
⊢ False

pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
n✝ : ℕ
h : n < n✝ + 1
hx₂ : x ∈ s.restrictNonposSeq i (n✝ + 1)
⊢ False

Tactic:
;

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
h : n < 0
hx₂ : x ∈ s.restrictNonposSeq i 0
⊢ False

case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
n✝ : ℕ
h : n < n✝ + 1
hx₂ : x ∈ s.restrictNonposSeq i (n✝ + 1)
⊢ False
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case inl
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : n < m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

Tactic:
restrictNonposSeq_disjoint' h

Goal state after:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : n < m
⊢ ∅ = ∅
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case inr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : m < n
⊢ s.restrictNonposSeq i m ∩ s.restrictNonposSeq i n = ∅

Tactic:
restrictNonposSeq_disjoint' h

Goal state after:
case inr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : m < n
⊢ ∅ = ∅
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ((-v).restrict i) j = (-v.restrict i) j

Tactic:
;

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ((-v).restrict i) j = (-v.restrict i) j
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
⊢ (if 0 ≤ ↑r then (↑r).toNNReal • j else -((-↑r).toNNReal • j)) = r • j

Tactic:
if_pos (NNReal.coe_nonneg r),

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
⊢ (↑r).toNNReal • j = r • j
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg
α : 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 : ℕ
⊢ 0 ≤ s (⋃ (_ : l < k), s.restrictNonposSeq i l)

Tactic:
;

Goal state after:
case neg
α : 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 : ℕ
⊢ 0 ≤ s (⋃ (_ : l < k), s.restrictNonposSeq i l)
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.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)
l : ℕ
h : ¬l < k
x✝ : α
⊢ x✝ ∈ ⋃ (_ : l < k), s.restrictNonposSeq i l ↔ x✝ ∈ ∅

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)
l : ℕ
h : ¬l < k
x✝ : α
⊢ x✝ ∈ ⋃ (_ : l < k), s.restrictNonposSeq i l ↔ x✝ ∈ ∅
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg.hm
α : 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)
i✝ : ℕ
⊢ MeasurableSet (⋃ (_ : i✝ < k), s.restrictNonposSeq i i✝)

Tactic:
;

Goal state after:
case neg.hm
α : 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)
i✝ : ℕ
⊢ MeasurableSet (⋃ (_ : i✝ < k), s.restrictNonposSeq i i✝)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : s ≤[i] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : s ≤[i] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ¬∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

Tactic:
;

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ¬∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : AddLeftMono M
inst✝ : ContinuousAdd M
x✝² x✝¹ x✝ : VectorMeasure α M
h : x✝¹ ≤ x✝
i : Set α
hi : MeasurableSet i
⊢ x✝² i + x✝¹ i ≤ x✝² i + x✝ i

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : AddLeftMono M
inst✝ : ContinuousAdd M
x✝² x✝¹ x✝ : VectorMeasure α M
h : x✝¹ ≤ x✝
i : Set α
hi : MeasurableSet i
⊢ x✝² i + x✝¹ i ≤ x✝² i + x✝ i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
x✝ : ℕ
⊢ ↑(bdd x✝) = ↑(bdd x✝) + 1 + -1

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
x✝ : ℕ
⊢ ↑(bdd x✝) = ↑(bdd x✝) + 1 + -1
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n ↦ ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
hnn : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ A → s j ≤ 0 j
⊢ False

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n ↦ ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
hnn : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ A → s j ≤ 0 j
⊢ False
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
ht₂ : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
;

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
ht₂ : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ IsFiniteMeasure (s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ IsFiniteMeasure (s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n ↦ ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : 0 E < s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < s E
hA' : A ⊆ i \ ⋃ l, ⋃ (_ : l ≤ k), s.restrictNonposSeq i l
⊢ ↑(s.findExistsOneDivLT (i \ ⋃ l, ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1) + 1 = ↑(bdd k)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n ↦ ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : 0 E < s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < s E
hA' : A ⊆ i \ ⋃ l, ⋃ (_ : l ≤ k), s.restrictNonposSeq i l
⊢ ↑(s.findExistsOneDivLT (i \ ⋃ l, ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1) + 1 = ↑(bdd k)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mp.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, s t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, t t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ s.totalVariation u = 0

Tactic:
rw [totalVariation, Measure.add_apply, hipos, hineg, toMeasureOfZeroLE_apply _ _ _ hmeas,
        toMeasureOfLEZero_apply _ _ _ hmeas]
      simp [hu₁ _ Set.inter_subset_right]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
⊢ { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯, not_measurable' := ⋯,
        m_iUnion' := ⋯ }
      s =
    ∫ (x : α) in s, f x ∂μ

Tactic:
;

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
⊢ { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0, empty' := ⋯, not_measurable' := ⋯,
        m_iUnion' := ⋯ }
      s =
    ∫ (x : α) in s, f x ∂μ
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᵐ[μ] g
hf : ¬Integrable f μ
hg : Integrable g μ
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᵐ[μ] g
hf : ¬Integrable f μ
hg : Integrable g μ
⊢ False
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure +
      μ.withDensityᵥ (s.rnDeriv μ) =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure

Tactic:
rnDeriv_def,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure +
      μ.withDensityᵥ fun x ↦
        (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, s.rnDeriv μ x ∂μ = s i

Tactic:
rnDeriv_def,

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i,
      (fun x ↦
          (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal)
        x ∂μ =
    s i