[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ↑v = ↑w
⊢ v = w
[PROOFSTEP]
cases v
[GOAL]
case mk
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
w : VectorMeasure α M
measureOf'✝ : Set α → M
empty'✝ : measureOf'✝ ∅ = 0
not_measurable'✝ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'✝ i = 0
m_iUnion'✝ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun i => measureOf'✝ (f i)) (measureOf'✝ (⋃ (i : ℕ), f i))
h : ↑{ measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ } = ↑w
⊢ { measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ } = w
[PROOFSTEP]
cases w
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
measureOf'✝¹ : Set α → M
empty'✝¹ : measureOf'✝¹ ∅ = 0
not_measurable'✝¹ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'✝¹ i = 0
m_iUnion'✝¹ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun i => measureOf'✝¹ (f i)) (measureOf'✝¹ (⋃ (i : ℕ), f i))
measureOf'✝ : Set α → M
empty'✝ : measureOf'✝ ∅ = 0
not_measurable'✝ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'✝ i = 0
m_iUnion'✝ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun i => measureOf'✝ (f i)) (measureOf'✝ (⋃ (i : ℕ), f i))
h :
  ↑{ measureOf' := measureOf'✝¹, empty' := empty'✝¹, not_measurable' := not_measurable'✝¹, m_iUnion' := m_iUnion'✝¹ } =
    ↑{ measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ }
⊢ { measureOf' := measureOf'✝¹, empty' := empty'✝¹, not_measurable' := not_measurable'✝¹, m_iUnion' := m_iUnion'✝¹ } =
    { measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w ↔ ∀ (i : Set α), ↑v i = ↑w i
[PROOFSTEP]
rw [← coe_injective.eq_iff, Function.funext_iff]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w ↔ ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w → ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
[PROOFSTEP]
rintro rfl _ _
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑v i✝ = ↑v i✝
[PROOFSTEP]
rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i) → v = w
[PROOFSTEP]
rw [ext_iff']
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ (∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i) → ∀ (i : Set α), ↑v i = ↑w i
[PROOFSTEP]
intro h i
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
i : Set α
⊢ ↑v i = ↑w i
[PROOFSTEP]
by_cases hi : MeasurableSet i
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
i : Set α
hi : MeasurableSet i
⊢ ↑v i = ↑w i
[PROOFSTEP]
exact h i hi
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
i : Set α
hi : ¬MeasurableSet i
⊢ ↑v i = ↑w i
[PROOFSTEP]
simp_rw [not_measurable _ hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
[PROOFSTEP]
cases nonempty_encodable β
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
[PROOFSTEP]
set g := fun i : ℕ => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b with hg
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
[PROOFSTEP]
have hg₁ : ∀ i, MeasurableSet (g i) := fun _ => MeasurableSet.iUnion fun b => MeasurableSet.iUnion fun _ => hf₁ b
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
[PROOFSTEP]
have hg₂ : Pairwise (Disjoint on g) := Encodable.iUnion_decode₂_disjoint_on hf₂
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
[PROOFSTEP]
have := v.of_disjoint_iUnion_nat hg₁ hg₂
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (i : ℕ), g i) = ∑' (i : ℕ), ↑v (g i)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
[PROOFSTEP]
rw [hg, Encodable.iUnion_decode₂] at this 
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
[PROOFSTEP]
have hg₃ : (fun i : β => v (f i)) = fun i => v (g (Encodable.encode i)) :=
  by
  ext x
  rw [hg]
  simp only
  congr
  ext y
  simp only [exists_prop, Set.mem_iUnion, Option.mem_def]
  constructor
  · intro hy
    refine' ⟨x, (Encodable.decode₂_is_partial_inv _ _).2 rfl, hy⟩
  · rintro ⟨b, hb₁, hb₂⟩
    rw [Encodable.decode₂_is_partial_inv _ _] at hb₁ 
    rwa [← Encodable.encode_injective hb₁]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
⊢ (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ ↑v (f x) = ↑v (g (Encodable.encode x))
[PROOFSTEP]
rw [hg]
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ ↑v (f x) = ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) (Encodable.encode x))
[PROOFSTEP]
simp only
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ ↑v (f x) = ↑v (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β (Encodable.encode x)), f b)
[PROOFSTEP]
congr
[GOAL]
case h.e_a
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
⊢ f x = ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β (Encodable.encode x)), f b
[PROOFSTEP]
ext y
[GOAL]
case h.e_a.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ y ∈ f x ↔ y ∈ ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β (Encodable.encode x)), f b
[PROOFSTEP]
simp only [exists_prop, Set.mem_iUnion, Option.mem_def]
[GOAL]
case h.e_a.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ y ∈ f x ↔ ∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i
[PROOFSTEP]
constructor
[GOAL]
case h.e_a.h.mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ y ∈ f x → ∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i
[PROOFSTEP]
intro hy
[GOAL]
case h.e_a.h.mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
hy : y ∈ f x
⊢ ∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i
[PROOFSTEP]
refine' ⟨x, (Encodable.decode₂_is_partial_inv _ _).2 rfl, hy⟩
[GOAL]
case h.e_a.h.mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
⊢ (∃ i, Encodable.decode₂ β (Encodable.encode x) = Option.some i ∧ y ∈ f i) → y ∈ f x
[PROOFSTEP]
rintro ⟨b, hb₁, hb₂⟩
[GOAL]
case h.e_a.h.mpr.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
b : β
hb₁ : Encodable.decode₂ β (Encodable.encode x) = Option.some b
hb₂ : y ∈ f b
⊢ y ∈ f x
[PROOFSTEP]
rw [Encodable.decode₂_is_partial_inv _ _] at hb₁ 
[GOAL]
case h.e_a.h.mpr.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
x : β
y : α
b : β
hb₁ : Encodable.encode b = Encodable.encode x
hb₂ : y ∈ f b
⊢ y ∈ f x
[PROOFSTEP]
rwa [← Encodable.encode_injective hb₁]
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ (i : β), f i))
[PROOFSTEP]
rw [Summable.hasSum_iff, this, ← tsum_iUnion_decode₂]
[GOAL]
case intro.m0
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ ↑v ∅ = 0
[PROOFSTEP]
exact v.empty
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable fun i => ↑v (f i)
[PROOFSTEP]
rw [hg₃]
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable fun i => ↑v (g (Encodable.encode i))
[PROOFSTEP]
change Summable ((fun i => v (g i)) ∘ Encodable.encode)
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable ((fun i => ↑v (g i)) ∘ Encodable.encode)
[PROOFSTEP]
rw [Function.Injective.summable_iff Encodable.encode_injective]
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ Summable fun i => ↑v (g i)
[PROOFSTEP]
exact (v.m_iUnion hg₁ hg₂).summable
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
⊢ ∀ (x : ℕ), ¬x ∈ range Encodable.encode → ↑v (g x) = 0
[PROOFSTEP]
intro x hx
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ¬x ∈ range Encodable.encode
⊢ ↑v (g x) = 0
[PROOFSTEP]
convert v.empty
[GOAL]
case h.e'_2.h.e'_7
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ¬x ∈ range Encodable.encode
⊢ g x = ∅
[PROOFSTEP]
simp only [Set.iUnion_eq_empty, Option.mem_def, not_exists, Set.mem_range] at hx ⊢
[GOAL]
case h.e'_2.h.e'_7
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ∀ (x_1 : β), ¬Encodable.encode x_1 = x
⊢ ∀ (i : β), Encodable.decode₂ β x = Option.some i → f i = ∅
[PROOFSTEP]
intro i hi
[GOAL]
case h.e'_2.h.e'_7
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
v : VectorMeasure α M
f✝ : ℕ → Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
val✝ : Encodable β
g : ℕ → Set α := fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg : g = fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
this : ↑v (⋃ (b : β), f b) = ∑' (i : ℕ), ↑v ((fun i => ⋃ (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) i)
hg₃ : (fun i => ↑v (f i)) = fun i => ↑v (g (Encodable.encode i))
x : ℕ
hx : ∀ (x_1 : β), ¬Encodable.encode x_1 = x
i : β
hi : Encodable.decode₂ β x = Option.some i
⊢ f i = ∅
[PROOFSTEP]
exact False.elim ((hx i) ((Encodable.decode₂_is_partial_inv _ _).1 hi))
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ↑v (A ∪ B) = ↑v A + ↑v B
[PROOFSTEP]
rw [Set.union_eq_iUnion, of_disjoint_iUnion, tsum_fintype, Fintype.sum_bool, cond, cond]
[GOAL]
case hf₁
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∀ (i : Bool), MeasurableSet (bif i then A else B)
case hf₂
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ Pairwise (Disjoint on fun b => bif b then A else B)
[PROOFSTEP]
exacts [fun b => Bool.casesOn b hB hA, pairwise_disjoint_on_bool.2 h]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
⊢ ↑v A + ↑v (B \ A) = ↑v B
[PROOFSTEP]
rw [← of_union (@Set.disjoint_sdiff_right _ A B) hA (hB.diff hA), Set.union_diff_cancel h]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M✝ : Type u_3
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : TopologicalSpace M✝
inst✝³ : T2Space M✝
v✝ : VectorMeasure α M✝
f : ℕ → Set α
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
⊢ ↑v (B \ A) = ↑v B - ↑v A
[PROOFSTEP]
rw [← of_add_of_diff hA hB h, add_sub_cancel']
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B) + ↑v B = ↑v A
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v A = ↑v (A \ B) + ↑v B
[PROOFSTEP]
calc
  v A = v (A \ B ∪ A ∩ B) := by simp only [Set.diff_union_inter]
  _ = v (A \ B) + v (A ∩ B) := by
    rw [of_union]
    · rw [disjoint_comm]
      exact Set.disjoint_of_subset_left (A.inter_subset_right B) disjoint_sdiff_self_right
    · exact hA.diff hB
    · exact hA.inter hB
  _ = v (A \ B) + v (A ∩ B ∪ B \ A) := by
    rw [of_union, h', add_zero]
    · exact Set.disjoint_of_subset_left (A.inter_subset_left B) disjoint_sdiff_self_right
    · exact hA.inter hB
    · exact hB.diff hA
  _ = v (A \ B) + v B := by rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v A = ↑v (A \ B ∪ A ∩ B)
[PROOFSTEP]
simp only [Set.diff_union_inter]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B ∪ A ∩ B) = ↑v (A \ B) + ↑v (A ∩ B)
[PROOFSTEP]
rw [of_union]
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A \ B) (A ∩ B)
[PROOFSTEP]
rw [disjoint_comm]
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A ∩ B) (A \ B)
[PROOFSTEP]
exact Set.disjoint_of_subset_left (A.inter_subset_right B) disjoint_sdiff_self_right
[GOAL]
case hA
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A \ B)
[PROOFSTEP]
exact hA.diff hB
[GOAL]
case hB
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A ∩ B)
[PROOFSTEP]
exact hA.inter hB
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B) + ↑v (A ∩ B) = ↑v (A \ B) + ↑v (A ∩ B ∪ B \ A)
[PROOFSTEP]
rw [of_union, h', add_zero]
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A ∩ B) (B \ A)
[PROOFSTEP]
exact Set.disjoint_of_subset_left (A.inter_subset_left B) disjoint_sdiff_self_right
[GOAL]
case hA
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A ∩ B)
[PROOFSTEP]
exact hA.inter hB
[GOAL]
case hB
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (B \ A)
[PROOFSTEP]
exact hB.diff hA
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B) + ↑v (A ∩ B ∪ B \ A) = ↑v (A \ B) + ↑v B
[PROOFSTEP]
rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ ↑s A
hB₂ : 0 ≤ ↑s B
hAB : ↑s (A ∪ B) = 0
⊢ ↑s A = 0
[PROOFSTEP]
rw [of_union h hA₁ hB₁] at hAB 
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ ↑s A
hB₂ : 0 ≤ ↑s B
hAB : ↑s A + ↑s B = 0
⊢ ↑s A = 0
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : ↑s A ≤ 0
hB₂ : ↑s B ≤ 0
hAB : ↑s (A ∪ B) = 0
⊢ ↑s A = 0
[PROOFSTEP]
rw [of_union h hA₁ hB₁] at hAB 
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : ↑s A ≤ 0
hB₂ : ↑s B ≤ 0
hAB : ↑s A + ↑s B = 0
⊢ ↑s A = 0
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
⊢ (r • ↑v) ∅ = 0
[PROOFSTEP]
rw [Pi.smul_apply, empty, smul_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ (r • ↑v) x✝ = 0
[PROOFSTEP]
rw [Pi.smul_apply, v.not_measurable hi, smul_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
x✝ : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (x✝ i)
hf₂ : Pairwise (Disjoint on x✝)
⊢ HasSum (fun i => (r • ↑v) (x✝ i)) ((r • ↑v) (⋃ (i : ℕ), x✝ i))
[PROOFSTEP]
exact HasSum.const_smul _ (v.m_iUnion hf₁ hf₂)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
⊢ (↑v + ↑w) ∅ = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ (↑v + ↑w) x✝ = 0
[PROOFSTEP]
rw [Pi.add_apply, v.not_measurable hi, w.not_measurable hi, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
⊢ (-↑v) ∅ = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ (-↑v) x✝ = 0
[PROOFSTEP]
rw [Pi.neg_apply, neg_eq_zero, v.not_measurable hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
⊢ (↑v - ↑w) ∅ = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ (↑v - ↑w) x✝ = 0
[PROOFSTEP]
rw [Pi.sub_apply, v.not_measurable hi, w.not_measurable hi, sub_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
⊢ (fun i => if MeasurableSet i then ENNReal.toReal (↑↑μ i) else 0) ∅ = 0
[PROOFSTEP]
simp [μ.empty]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun i => (fun i => if MeasurableSet i then ENNReal.toReal (↑↑μ i) else 0) (f i))
    ((fun i => if MeasurableSet i then ENNReal.toReal (↑↑μ i) else 0) (⋃ (i : ℕ), f i))
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun i => if MeasurableSet (f i) then ENNReal.toReal (↑↑μ (f i)) else 0)
    (if MeasurableSet (⋃ (i : ℕ), f i) then ENNReal.toReal (↑↑μ (⋃ (i : ℕ), f i)) else 0)
[PROOFSTEP]
rw [μ.m_iUnion hf₁ hf₂, ENNReal.tsum_toReal_eq, if_pos (MeasurableSet.iUnion hf₁), Summable.hasSum_iff]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ (∑' (b : ℕ), if MeasurableSet (f b) then ENNReal.toReal (↑↑μ (f b)) else 0) = ∑' (a : ℕ), ENNReal.toReal (↑↑μ (f a))
[PROOFSTEP]
congr
[GOAL]
case e_f
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ (fun b => if MeasurableSet (f b) then ENNReal.toReal (↑↑μ (f b)) else 0) = fun a => ENNReal.toReal (↑↑μ (f a))
[PROOFSTEP]
ext n
[GOAL]
case e_f.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
n : ℕ
⊢ (if MeasurableSet (f n) then ENNReal.toReal (↑↑μ (f n)) else 0) = ENNReal.toReal (↑↑μ (f n))
[PROOFSTEP]
rw [if_pos (hf₁ n)]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ Summable fun i => if MeasurableSet (f i) then ENNReal.toReal (↑↑μ (f i)) else 0
[PROOFSTEP]
refine' @summable_of_nonneg_of_le _ (ENNReal.toReal ∘ μ ∘ f) _ _ _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ ∀ (b : ℕ), 0 ≤ if MeasurableSet (f b) then ENNReal.toReal (↑↑μ (f b)) else 0
[PROOFSTEP]
intro
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
b✝ : ℕ
⊢ 0 ≤ if MeasurableSet (f b✝) then ENNReal.toReal (↑↑μ (f b✝)) else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
b✝ : ℕ
h✝ : MeasurableSet (f b✝)
⊢ 0 ≤ ENNReal.toReal (↑↑μ (f b✝))
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
b✝ : ℕ
h✝ : ¬MeasurableSet (f b✝)
⊢ 0 ≤ 0
[PROOFSTEP]
exacts [ENNReal.toReal_nonneg, le_rfl]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ ∀ (b : ℕ), (if MeasurableSet (f b) then ENNReal.toReal (↑↑μ (f b)) else 0) ≤ (ENNReal.toReal ∘ ↑↑μ ∘ f) b
[PROOFSTEP]
intro
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
b✝ : ℕ
⊢ (if MeasurableSet (f b✝) then ENNReal.toReal (↑↑μ (f b✝)) else 0) ≤ (ENNReal.toReal ∘ ↑↑μ ∘ f) b✝
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
b✝ : ℕ
h✝ : MeasurableSet (f b✝)
⊢ ENNReal.toReal (↑↑μ (f b✝)) ≤ (ENNReal.toReal ∘ ↑↑μ ∘ f) b✝
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
b✝ : ℕ
h✝ : ¬MeasurableSet (f b✝)
⊢ 0 ≤ (ENNReal.toReal ∘ ↑↑μ ∘ f) b✝
[PROOFSTEP]
exacts [le_rfl, ENNReal.toReal_nonneg]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ Summable (ENNReal.toReal ∘ ↑↑μ ∘ f)
[PROOFSTEP]
exact summable_measure_toReal hf₁ hf₂
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ ∀ (a : ℕ), ↑↑μ (f a) ≠ ⊤
[PROOFSTEP]
intro a ha
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
a : ℕ
ha : ↑↑μ (f a) = ⊤
⊢ False
[PROOFSTEP]
apply ne_of_lt hμ.measure_univ_lt_top
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
a : ℕ
ha : ↑↑μ (f a) = ⊤
⊢ ↑↑μ univ = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← ha]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
a : ℕ
ha : ↑↑μ (f a) = ⊤
⊢ ↑↑μ (f a) ≤ ↑↑μ univ
[PROOFSTEP]
exact measure_mono (Set.subset_univ _)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ = ν
⊢ toSignedMeasure μ = toSignedMeasure ν
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ toSignedMeasure μ = toSignedMeasure ν ↔ μ = ν
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
⊢ μ = ν
[PROOFSTEP]
ext1 i hi
[GOAL]
case refine'_1.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑↑μ i = ↑↑ν i
[PROOFSTEP]
have : μ.toSignedMeasure i = ν.toSignedMeasure i := by rw [h]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure μ) i = ↑(toSignedMeasure ν) i
[PROOFSTEP]
rw [h]
[GOAL]
case refine'_1.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
i : Set α
hi : MeasurableSet i
this : ↑(toSignedMeasure μ) i = ↑(toSignedMeasure ν) i
⊢ ↑↑μ i = ↑↑ν i
[PROOFSTEP]
rwa [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, ENNReal.toReal_eq_toReal] at this 
[GOAL]
case refine'_1.h.ha
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
i : Set α
hi : MeasurableSet i
this : ENNReal.toReal (↑↑μ i) = ENNReal.toReal (↑↑ν i)
⊢ ↑↑μ i ≠ ⊤
[PROOFSTEP]
exact measure_ne_top _ _
[GOAL]
case refine'_1.h.hb
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : toSignedMeasure μ = toSignedMeasure ν
i : Set α
hi : MeasurableSet i
this : ENNReal.toReal (↑↑μ i) = ENNReal.toReal (↑↑ν i)
⊢ ↑↑ν i ≠ ⊤
[PROOFSTEP]
exact measure_ne_top _ _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ = ν
⊢ toSignedMeasure μ = toSignedMeasure ν
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
⊢ toSignedMeasure 0 = 0
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
i : Set α
a✝ : MeasurableSet i
⊢ ↑(toSignedMeasure 0) i = ↑0 i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ toSignedMeasure (μ + ν) = toSignedMeasure μ + toSignedMeasure ν
[PROOFSTEP]
ext i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure (μ + ν)) i = ↑(toSignedMeasure μ + toSignedMeasure ν) i
[PROOFSTEP]
rw [toSignedMeasure_apply_measurable hi, add_apply,
  ENNReal.toReal_add (ne_of_lt (measure_lt_top _ _)) (ne_of_lt (measure_lt_top _ _)), VectorMeasure.add_apply,
  toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
⊢ toSignedMeasure (r • μ) = r • toSignedMeasure μ
[PROOFSTEP]
ext i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure (r • μ)) i = ↑(r • toSignedMeasure μ) i
[PROOFSTEP]
rw [toSignedMeasure_apply_measurable hi, VectorMeasure.smul_apply, toSignedMeasure_apply_measurable hi, coe_smul,
  Pi.smul_apply, ENNReal.toReal_smul]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
⊢ (fun i => if MeasurableSet i then ↑↑μ i else 0) ∅ = 0
[PROOFSTEP]
simp [μ.empty]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x✝ : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (x✝ i)
hf₂ : Pairwise (Disjoint on x✝)
⊢ HasSum (fun i => (fun i => if MeasurableSet i then ↑↑μ i else 0) (x✝ i))
    ((fun i => if MeasurableSet i then ↑↑μ i else 0) (⋃ (i : ℕ), x✝ i))
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x✝ : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (x✝ i)
hf₂ : Pairwise (Disjoint on x✝)
⊢ HasSum (fun i => if MeasurableSet (x✝ i) then ↑↑μ (x✝ i) else 0)
    (if MeasurableSet (⋃ (i : ℕ), x✝ i) then ↑↑μ (⋃ (i : ℕ), x✝ i) else 0)
[PROOFSTEP]
rw [Summable.hasSum_iff ENNReal.summable, if_pos (MeasurableSet.iUnion hf₁), MeasureTheory.measure_iUnion hf₂ hf₁]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x✝ : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (x✝ i)
hf₂ : Pairwise (Disjoint on x✝)
⊢ (∑' (b : ℕ), if MeasurableSet (x✝ b) then ↑↑μ (x✝ b) else 0) = ∑' (i : ℕ), ↑↑μ (x✝ i)
[PROOFSTEP]
exact tsum_congr fun n => if_pos (hf₁ n)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
⊢ toENNRealVectorMeasure 0 = 0
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
i : Set α
a✝ : MeasurableSet i
⊢ ↑(toENNRealVectorMeasure 0) i = ↑0 i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
⊢ toENNRealVectorMeasure (μ + ν) = toENNRealVectorMeasure μ + toENNRealVectorMeasure ν
[PROOFSTEP]
refine' MeasureTheory.VectorMeasure.ext fun i hi => _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ ↑(toENNRealVectorMeasure (μ + ν)) i = ↑(toENNRealVectorMeasure μ + toENNRealVectorMeasure ν) i
[PROOFSTEP]
rw [toENNRealVectorMeasure_apply_measurable hi, add_apply, VectorMeasure.add_apply,
  toENNRealVectorMeasure_apply_measurable hi, toENNRealVectorMeasure_apply_measurable hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure μ - toSignedMeasure ν) i = ENNReal.toReal (↑↑μ i) - ENNReal.toReal (↑↑ν i)
[PROOFSTEP]
rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi, Measure.toSignedMeasure_apply_measurable hi,
  sub_eq_add_neg]
[GOAL]
α : Type u_1
β : Type u_2
m✝ m : MeasurableSpace α
v : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑↑(ennrealToMeasure v) s = ↑v s
[PROOFSTEP]
rw [ennrealToMeasure, ofMeasurable_apply _ hs]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝ : MeasurableSpace α
x✝ : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑(toENNRealVectorMeasure (ennrealToMeasure x✝)) s = ↑x✝ s
[PROOFSTEP]
rw [toENNRealVectorMeasure_apply_measurable hs, ennrealToMeasure_apply hs]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝ : MeasurableSpace α
x✝ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(ennrealToMeasure (toENNRealVectorMeasure x✝)) s = ↑↑x✝ s
[PROOFSTEP]
rw [ennrealToMeasure_apply hs, toENNRealVectorMeasure_apply_measurable hs]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ (fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0) ∅ = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → Set β⦄,
    (∀ (i : ℕ), MeasurableSet (f_1 i)) →
      Pairwise (Disjoint on f_1) →
        HasSum (fun i => (fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0) (f_1 i))
          ((fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0) (⋃ (i : ℕ), f_1 i))
[PROOFSTEP]
intro g hg₁ hg₂
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
⊢ HasSum (fun i => (fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0) (g i))
    ((fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0) (⋃ (i : ℕ), g i))
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
⊢ HasSum (fun i => if MeasurableSet (g i) then ↑v (f ⁻¹' g i) else 0)
    (if MeasurableSet (⋃ (i : ℕ), g i) then ↑v (f ⁻¹' ⋃ (i : ℕ), g i) else 0)
[PROOFSTEP]
convert v.m_iUnion (fun i => hf (hg₁ i)) fun i j hij => (hg₂ hij).preimage _
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
x✝ : ℕ
⊢ (if MeasurableSet (g x✝) then ↑v (f ⁻¹' g x✝) else 0) = ↑v (f ⁻¹' g x✝)
[PROOFSTEP]
rw [if_pos (hg₁ _)]
[GOAL]
case h.e'_6
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
⊢ (if MeasurableSet (⋃ (i : ℕ), g i) then ↑v (f ⁻¹' ⋃ (i : ℕ), g i) else 0) = ↑v (⋃ (i : ℕ), f ⁻¹' g i)
[PROOFSTEP]
rw [Set.preimage_iUnion, if_pos (MeasurableSet.iUnion hg₁)]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑(map v f) s = ↑v (f ⁻¹' s)
[PROOFSTEP]
rw [map, dif_pos hf]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0,
          empty' := (_ : (if MeasurableSet ∅ then ↑v (f ⁻¹' ∅) else 0) = 0),
          not_measurable' := (_ : ∀ (i : Set β), ¬MeasurableSet i → (if MeasurableSet i then ↑v (f ⁻¹' i) else 0) = 0),
          m_iUnion' :=
            (_ :
              ∀ ⦃g : ℕ → Set β⦄,
                (∀ (i : ℕ), MeasurableSet (g i)) →
                  Pairwise (Disjoint on g) →
                    HasSum (fun i => (fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0) (g i))
                      ((fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0) (⋃ (i : ℕ), g i))) }
      s =
    ↑v (f ⁻¹' s)
[PROOFSTEP]
exact if_pos hs
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(map v id) i = ↑v i
[PROOFSTEP]
rw [map_apply v measurable_id hi, Set.preimage_id]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
⊢ map 0 f = 0
[PROOFSTEP]
by_cases hf : Measurable f
[GOAL]
case pos
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ map 0 f = 0
[PROOFSTEP]
ext i hi
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ↑(map 0 f) i = ↑0 i
[PROOFSTEP]
rw [map_apply _ hf hi, zero_apply, zero_apply]
[GOAL]
case neg
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : ¬Measurable f
⊢ map 0 f = 0
[PROOFSTEP]
exact dif_neg hf
[GOAL]
α : Type u_1
β : Type u_2
m inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
v✝ : VectorMeasure α M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
f : M →+ N
hf : Continuous ↑f
⊢ (fun s => ↑f (↑v s)) ∅ = 0
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
m inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
v✝ : VectorMeasure α M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
f : M →+ N
hf : Continuous ↑f
⊢ ↑f (↑v ∅) = 0
[PROOFSTEP]
rw [empty, AddMonoidHom.map_zero]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
v✝ : VectorMeasure α M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
f : M →+ N
hf : Continuous ↑f
i : Set α
hi : ¬MeasurableSet i
⊢ (fun s => ↑f (↑v s)) i = 0
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
m inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
v✝ : VectorMeasure α M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
f : M →+ N
hf : Continuous ↑f
i : Set α
hi : ¬MeasurableSet i
⊢ ↑f (↑v i) = 0
[PROOFSTEP]
rw [not_measurable v hi, AddMonoidHom.map_zero]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
v : VectorMeasure α M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
⊢ mapRange v (AddMonoidHom.id M) (_ : Continuous id) = v
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
m inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
v : VectorMeasure α M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange v (AddMonoidHom.id M) (_ : Continuous id)) i✝ = ↑v i✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
m inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
v : VectorMeasure α M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
f : M →+ N
hf : Continuous ↑f
⊢ mapRange 0 f hf = 0
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
m inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
v : VectorMeasure α M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
f : M →+ N
hf : Continuous ↑f
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange 0 f hf) i✝ = ↑0 i✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
v✝ : VectorMeasure α M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousAdd N
v w : VectorMeasure α M
f : M →+ N
hf : Continuous ↑f
⊢ mapRange (v + w) f hf = mapRange v f hf + mapRange w f hf
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
m inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
v✝ : VectorMeasure α M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousAdd N
v w : VectorMeasure α M
f : M →+ N
hf : Continuous ↑f
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange (v + w) f hf) i✝ = ↑(mapRange v f hf + mapRange w f hf) i✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace β
M : Type u_3
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : TopologicalSpace M
v : VectorMeasure α 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✝³ : ContinuousAdd M
inst✝² : ContinuousAdd N
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousConstSMul R N
f : M →ₗ[R] N
hf : Continuous ↑f
⊢ ∀ (r : R) (x : VectorMeasure α M),
    AddHom.toFun
        { toFun := fun v => mapRange v (LinearMap.toAddMonoidHom f) hf,
          map_add' :=
            (_ :
              ∀ (x x_1 : VectorMeasure α M),
                mapRange (x + x_1) (LinearMap.toAddMonoidHom f) hf =
                  mapRange x (LinearMap.toAddMonoidHom f) hf + mapRange x_1 (LinearMap.toAddMonoidHom f) hf) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := fun v => mapRange v (LinearMap.toAddMonoidHom f) hf,
            map_add' :=
              (_ :
                ∀ (x x_1 : VectorMeasure α M),
                  mapRange (x + x_1) (LinearMap.toAddMonoidHom f) hf =
                    mapRange x (LinearMap.toAddMonoidHom f) hf + mapRange x_1 (LinearMap.toAddMonoidHom f) hf) }
          x
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
m inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace β
M : Type u_3
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : TopologicalSpace M
v : VectorMeasure α 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✝³ : ContinuousAdd M
inst✝² : ContinuousAdd N
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousConstSMul R N
f : M →ₗ[R] N
hf : Continuous ↑f
r✝ : R
x✝ : VectorMeasure α M
⊢ AddHom.toFun
      { toFun := fun v => mapRange v (LinearMap.toAddMonoidHom f) hf,
        map_add' :=
          (_ :
            ∀ (x x_1 : VectorMeasure α M),
              mapRange (x + x_1) (LinearMap.toAddMonoidHom f) hf =
                mapRange x (LinearMap.toAddMonoidHom f) hf + mapRange x_1 (LinearMap.toAddMonoidHom f) hf) }
      (r✝ • x✝) =
    ↑(RingHom.id R) r✝ •
      AddHom.toFun
        { toFun := fun v => mapRange v (LinearMap.toAddMonoidHom f) hf,
          map_add' :=
            (_ :
              ∀ (x x_1 : VectorMeasure α M),
                mapRange (x + x_1) (LinearMap.toAddMonoidHom f) hf =
                  mapRange x (LinearMap.toAddMonoidHom f) hf + mapRange x_1 (LinearMap.toAddMonoidHom f) hf) }
        x✝
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
m inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace β
M : Type u_3
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : TopologicalSpace M
v : VectorMeasure α 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✝³ : ContinuousAdd M
inst✝² : ContinuousAdd N
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousConstSMul R N
f : M →ₗ[R] N
hf : Continuous ↑f
r✝ : R
x✝ : VectorMeasure α M
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(AddHom.toFun
          { toFun := fun v => mapRange v (LinearMap.toAddMonoidHom f) hf,
            map_add' :=
              (_ :
                ∀ (x x_1 : VectorMeasure α M),
                  mapRange (x + x_1) (LinearMap.toAddMonoidHom f) hf =
                    mapRange x (LinearMap.toAddMonoidHom f) hf + mapRange x_1 (LinearMap.toAddMonoidHom f) hf) }
          (r✝ • x✝))
      i✝ =
    ↑(↑(RingHom.id R) r✝ •
          AddHom.toFun
            { toFun := fun v => mapRange v (LinearMap.toAddMonoidHom f) hf,
              map_add' :=
                (_ :
                  ∀ (x x_1 : VectorMeasure α M),
                    mapRange (x + x_1) (LinearMap.toAddMonoidHom f) hf =
                      mapRange x (LinearMap.toAddMonoidHom f) hf + mapRange x_1 (LinearMap.toAddMonoidHom f) hf) }
            x✝)
      i✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (fun s => if MeasurableSet s then ↑v (s ∩ i) else 0) ∅ = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) →
        HasSum (fun i_1 => (fun s => if MeasurableSet s then ↑v (s ∩ i) else 0) (f i_1))
          ((fun s => if MeasurableSet s then ↑v (s ∩ i) else 0) (⋃ (i : ℕ), f i))
[PROOFSTEP]
intro f hf₁ hf₂
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun i_1 => (fun s => if MeasurableSet s then ↑v (s ∩ i) else 0) (f i_1))
    ((fun s => if MeasurableSet s then ↑v (s ∩ i) else 0) (⋃ (i : ℕ), f i))
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun i_1 => if MeasurableSet (f i_1) then ↑v (f i_1 ∩ i) else 0)
    (if MeasurableSet (⋃ (i : ℕ), f i) then ↑v ((⋃ (i : ℕ), f i) ∩ i) else 0)
[PROOFSTEP]
convert v.m_iUnion (fun n => (hf₁ n).inter hi) (hf₂.mono fun i j => Disjoint.mono inf_le_left inf_le_left)
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
x✝ : ℕ
⊢ (if MeasurableSet (f x✝) then ↑v (f x✝ ∩ i) else 0) = ↑v (f x✝ ∩ i)
[PROOFSTEP]
rw [if_pos (hf₁ _)]
[GOAL]
case h.e'_6
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ (if MeasurableSet (⋃ (i : ℕ), f i) then ↑v ((⋃ (i : ℕ), f i) ∩ i) else 0) = ↑v (⋃ (i_1 : ℕ), f i_1 ∩ i)
[PROOFSTEP]
rw [Set.iUnion_inter, if_pos (MeasurableSet.iUnion hf₁)]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict v i) j = ↑v (j ∩ i)
[PROOFSTEP]
rw [restrict, dif_pos hi]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ↑v (s ∩ i) else 0,
          empty' := (_ : (if MeasurableSet ∅ then ↑v (∅ ∩ i) else 0) = 0),
          not_measurable' :=
            (_ : ∀ (i_1 : Set α), ¬MeasurableSet i_1 → (if MeasurableSet i_1 then ↑v (i_1 ∩ i) else 0) = 0),
          m_iUnion' :=
            (_ :
              ∀ ⦃f : ℕ → Set α⦄,
                (∀ (i : ℕ), MeasurableSet (f i)) →
                  Pairwise (Disjoint on f) →
                    HasSum (fun i_1 => (fun s => if MeasurableSet s then ↑v (s ∩ i) else 0) (f i_1))
                      ((fun s => if MeasurableSet s then ↑v (s ∩ i) else 0) (⋃ (i : ℕ), f i))) }
      j =
    ↑v (j ∩ i)
[PROOFSTEP]
exact if_pos hj
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
hij : j ⊆ i
⊢ ↑(restrict v i) j = ↑v j
[PROOFSTEP]
rw [restrict_apply v hi hj, Set.inter_eq_left_iff_subset.2 hij]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(restrict v ∅) i = ↑0 i
[PROOFSTEP]
rw [restrict_apply v MeasurableSet.empty hi, Set.inter_empty, v.empty, zero_apply]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(restrict v univ) i = ↑v i
[PROOFSTEP]
rw [restrict_apply v MeasurableSet.univ hi, Set.inter_univ]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
⊢ restrict 0 i = 0
[PROOFSTEP]
by_cases hi : MeasurableSet i
[GOAL]
case pos
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ restrict 0 i = 0
[PROOFSTEP]
ext j hj
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict 0 i) j = ↑0 j
[PROOFSTEP]
rw [restrict_apply 0 hi hj]
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑0 (j ∩ i) = ↑0 j
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ restrict 0 i = 0
[PROOFSTEP]
exact dif_neg hi
[GOAL]
α : Type u_1
β : Type u_2
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
⊢ map (v + w) f = map v f + map w f
[PROOFSTEP]
by_cases hf : Measurable f
[GOAL]
case pos
α : Type u_1
β : Type u_2
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ map (v + w) f = map v f + map w f
[PROOFSTEP]
ext i hi
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ↑(map (v + w) f) i = ↑(map v f + map w f) i
[PROOFSTEP]
simp [map_apply _ hf hi]
[GOAL]
case neg
α : Type u_1
β : Type u_2
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : ¬Measurable f
⊢ map (v + w) f = map v f + map w f
[PROOFSTEP]
simp [map, dif_neg hf]
[GOAL]
α : Type u_1
β : Type u_2
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
⊢ restrict (v + w) i = restrict v i + restrict w i
[PROOFSTEP]
by_cases hi : MeasurableSet i
[GOAL]
case pos
α : Type u_1
β : Type u_2
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ restrict (v + w) i = restrict v i + restrict w i
[PROOFSTEP]
ext j hj
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict (v + w) i) j = ↑(restrict v i + restrict w i) j
[PROOFSTEP]
simp [restrict_apply _ hi hj]
[GOAL]
case neg
α : Type u_1
β : Type u_2
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ restrict (v + w) i = restrict v i + restrict w i
[PROOFSTEP]
simp [restrict_not_measurable _ hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
⊢ map (c • v) f = c • map v f
[PROOFSTEP]
by_cases hf : Measurable f
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
⊢ map (c • v) f = c • map v f
[PROOFSTEP]
ext i hi
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ↑(map (c • v) f) i = ↑(c • map v f) i
[PROOFSTEP]
simp [map_apply _ hf hi]
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ map (c • v) f = c • map v f
[PROOFSTEP]
simp only [map, dif_neg hf]
  -- `smul_zero` does not work since we do not require `ContinuousAdd`
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ 0 = c • 0
[PROOFSTEP]
ext i
[GOAL]
case neg.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
i : Set β
a✝ : MeasurableSet i
⊢ ↑0 i = ↑(c • 0) i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
⊢ restrict (c • v) i = c • restrict v i
[PROOFSTEP]
by_cases hi : MeasurableSet i
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
⊢ restrict (c • v) i = c • restrict v i
[PROOFSTEP]
ext j hj
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict (c • v) i) j = ↑(c • restrict v i) j
[PROOFSTEP]
simp [restrict_apply _ hi hj]
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ restrict (c • v) i = c • restrict v i
[PROOFSTEP]
simp only [restrict_not_measurable _ hi]
  -- `smul_zero` does not work since we do not require `ContinuousAdd`
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ 0 = c • 0
[PROOFSTEP]
ext j
[GOAL]
case neg.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
j : Set α
a✝ : MeasurableSet j
⊢ ↑0 j = ↑(c • 0) j
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
u v w : VectorMeasure α M
⊢ v ≤ w ↔ ∀ (i : Set α), ↑v i ≤ ↑w i
[PROOFSTEP]
refine' ⟨fun h i => _, fun h i _ => h i⟩
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
u v w : VectorMeasure α M
h : v ≤ w
i : Set α
⊢ ↑v i ≤ ↑w i
[PROOFSTEP]
by_cases hi : MeasurableSet i
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
u v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : MeasurableSet i
⊢ ↑v i ≤ ↑w i
[PROOFSTEP]
exact h i hi
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
u v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
⊢ ↑v i ≤ ↑w i
[PROOFSTEP]
rw [v.not_measurable hi, w.not_measurable hi]
[GOAL]
α : Type u_1
β : Type u_2
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₂ : restrict v i ≤ restrict w i
j : Set α
hj : j ⊆ i
⊢ ↑v j ≤ ↑w j
[PROOFSTEP]
by_cases hj₁ : MeasurableSet j
[GOAL]
case pos
α : Type u_1
β : Type u_2
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₂ : restrict v i ≤ restrict w i
j : Set α
hj : j ⊆ i
hj₁ : MeasurableSet j
⊢ ↑v j ≤ ↑w j
[PROOFSTEP]
exact (restrict_le_restrict_iff _ _ hi).1 hi₂ hj₁ hj
[GOAL]
case neg
α : Type u_1
β : Type u_2
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₂ : restrict v i ≤ restrict w i
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ ↑v j ≤ ↑w j
[PROOFSTEP]
rw [v.not_measurable hj₁, w.not_measurable hj₁]
[GOAL]
α : Type u_1
β : Type u_2
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
⊢ restrict v i ≤ restrict w i
[PROOFSTEP]
by_cases hi : MeasurableSet i
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
⊢ restrict v i ≤ restrict w i
[PROOFSTEP]
exact (restrict_le_restrict_iff _ _ hi).2 h
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
⊢ restrict v i ≤ restrict w i
[PROOFSTEP]
rw [restrict_not_measurable v hi, restrict_not_measurable w hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ restrict v ∅ ≤ restrict w ∅
[PROOFSTEP]
intro j _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
j : Set α
a✝ : MeasurableSet j
⊢ ↑(restrict v ∅) j ≤ ↑(restrict w ∅) j
[PROOFSTEP]
rw [restrict_empty, restrict_empty]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ restrict v univ ≤ restrict w univ ↔ v ≤ w
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ restrict v univ ≤ restrict w univ → v ≤ w
[PROOFSTEP]
intro h s hs
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : restrict v univ ≤ restrict w univ
s : Set α
hs : MeasurableSet s
⊢ ↑v s ≤ ↑w s
[PROOFSTEP]
have := h s hs
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : restrict v univ ≤ restrict w univ
s : Set α
hs : MeasurableSet s
this : ↑(restrict v univ) s ≤ ↑(restrict w univ) s
⊢ ↑v s ≤ ↑w s
[PROOFSTEP]
rwa [restrict_apply _ MeasurableSet.univ hs, Set.inter_univ, restrict_apply _ MeasurableSet.univ hs, Set.inter_univ] at
  this 
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤ w → restrict v univ ≤ restrict w univ
[PROOFSTEP]
intro h s hs
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
s : Set α
hs : MeasurableSet s
⊢ ↑(restrict v univ) s ≤ ↑(restrict w univ) s
[PROOFSTEP]
rw [restrict_apply _ MeasurableSet.univ hs, Set.inter_univ, restrict_apply _ MeasurableSet.univ hs, Set.inter_univ]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
s : Set α
hs : MeasurableSet s
⊢ ↑v s ≤ ↑w s
[PROOFSTEP]
exact h s hs
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
⊢ restrict (-w) i ≤ restrict (-v) i
[PROOFSTEP]
intro j hj₁
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ ↑(restrict (-w) i) j ≤ ↑(restrict (-v) i) j
[PROOFSTEP]
rw [restrict_apply _ hi hj₁, restrict_apply _ hi hj₁, neg_apply, neg_apply]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ -↑w (j ∩ i) ≤ -↑v (j ∩ i)
[PROOFSTEP]
refine' neg_le_neg _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ ↑v (j ∩ i) ≤ ↑w (j ∩ i)
[PROOFSTEP]
rw [← restrict_apply _ hi hj₁, ← restrict_apply _ hi hj₁]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : TopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : restrict v i ≤ restrict w i
j : Set α
hj₁ : MeasurableSet j
⊢ ↑(restrict v i) j ≤ ↑(restrict w i) j
[PROOFSTEP]
exact h j hj₁
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
⊢ restrict v (⋃ (n : ℕ), f n) ≤ restrict w (⋃ (n : ℕ), f n)
[PROOFSTEP]
refine' restrict_le_restrict_of_subset_le v w fun a ha₁ ha₂ => _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
⊢ ↑v a ≤ ↑w a
[PROOFSTEP]
have ha₃ : ⋃ n, a ∩ disjointed f n = a := by rwa [← Set.inter_iUnion, iUnion_disjointed, Set.inter_eq_left_iff_subset]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
⊢ ⋃ (n : ℕ), a ∩ disjointed f n = a
[PROOFSTEP]
rwa [← Set.inter_iUnion, iUnion_disjointed, Set.inter_eq_left_iff_subset]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : ⋃ (n : ℕ), a ∩ disjointed f n = a
⊢ ↑v a ≤ ↑w a
[PROOFSTEP]
have ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n) :=
  (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
⊢ ↑v a ≤ ↑w a
[PROOFSTEP]
rw [← ha₃, v.of_disjoint_iUnion_nat _ ha₄, w.of_disjoint_iUnion_nat _ ha₄]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
[PROOFSTEP]
refine' tsum_le_tsum (fun n => (restrict_le_restrict_iff v w (hf₁ n)).1 (hf₂ n) _ _) _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)
[PROOFSTEP]
exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
n : ℕ
⊢ a ∩ disjointed f n ⊆ f n
[PROOFSTEP]
exact Set.Subset.trans (Set.inter_subset_right _ _) (disjointed_subset _ _)
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
⊢ Summable fun i => ↑v (a ∩ disjointed f i)
[PROOFSTEP]
refine' (v.m_iUnion (fun n => _) _).summable
[GOAL]
case refine'_3.refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)
[PROOFSTEP]
exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
[GOAL]
case refine'_3.refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
⊢ Pairwise (Disjoint on fun i => a ∩ disjointed f i)
[PROOFSTEP]
exact (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
⊢ Summable fun i => ↑w (a ∩ disjointed f i)
[PROOFSTEP]
refine' (w.m_iUnion (fun n => _) _).summable
[GOAL]
case refine'_4.refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)
[PROOFSTEP]
exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
[GOAL]
case refine'_4.refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
⊢ Pairwise (Disjoint on fun i => a ∩ disjointed f i)
[PROOFSTEP]
exact (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)
[PROOFSTEP]
exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
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)
[PROOFSTEP]
exact fun n => ha₁.inter (MeasurableSet.disjointed hf₁ n)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
⊢ restrict v (⋃ (b : β), f b) ≤ restrict w (⋃ (b : β), f b)
[PROOFSTEP]
cases nonempty_encodable β
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ restrict v (⋃ (b : β), f b) ≤ restrict w (⋃ (b : β), f b)
[PROOFSTEP]
rw [← Encodable.iUnion_decode₂]
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ restrict v (⋃ (i : ℕ) (b : β) (_ : b ∈ Encodable.decode₂ β i), f b) ≤
    restrict w (⋃ (i : ℕ) (b : β) (_ : b ∈ Encodable.decode₂ β i), f b)
[PROOFSTEP]
refine' restrict_le_restrict_iUnion v w _ _
[GOAL]
case intro.refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ ∀ (n : ℕ), MeasurableSet (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)
[PROOFSTEP]
intro n
[GOAL]
case intro.refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
⊢ MeasurableSet (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)
[PROOFSTEP]
measurability
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
⊢ ∀ (n : ℕ),
    restrict v (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b) ≤
      restrict w (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)
[PROOFSTEP]
intro n
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
⊢ restrict v (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b) ≤
    restrict w (⋃ (b : β) (_ : b ∈ Encodable.decode₂ β n), f b)
[PROOFSTEP]
cases' Encodable.decode₂ β n with b
[GOAL]
case intro.refine'_2.none
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
⊢ restrict v (⋃ (b : β) (_ : b ∈ none), f b) ≤ restrict w (⋃ (b : β) (_ : b ∈ none), f b)
[PROOFSTEP]
simp
[GOAL]
case intro.refine'_2.some
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : OrderedAddCommMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), restrict v (f b) ≤ restrict w (f b)
val✝ : Encodable β
n : ℕ
b : β
⊢ restrict v (⋃ (b_1 : β) (_ : b_1 ∈ Option.some b), f b_1) ≤ restrict w (⋃ (b_1 : β) (_ : b_1 ∈ Option.some b), f b_1)
[PROOFSTEP]
simp [hf₂ b]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ restrict v (i ∪ j) ≤ restrict w (i ∪ j)
[PROOFSTEP]
rw [Set.union_eq_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ restrict v (⋃ (b : Bool), bif b then i else j) ≤ restrict w (⋃ (b : Bool), bif b then i else j)
[PROOFSTEP]
refine' restrict_le_restrict_countable_iUnion v w _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ ∀ (b : Bool), MeasurableSet (bif b then i else j)
[PROOFSTEP]
measurability
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ ∀ (b : Bool), restrict v (bif b then i else j) ≤ restrict w (bif b then i else j)
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case refine'_2.false
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ restrict v (bif false then i else j) ≤ restrict w (bif false then i else j)
[PROOFSTEP]
simpa
[GOAL]
case refine'_2.true
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : restrict v i ≤ restrict w i
hj₁ : MeasurableSet j
hj₂ : restrict v j ≤ restrict w j
⊢ restrict v (bif true then i else j) ≤ restrict w (bif true then i else j)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₂ : restrict 0 i ≤ restrict v i
⊢ 0 ≤ ↑v i
[PROOFSTEP]
by_cases hi₁ : MeasurableSet i
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₂ : restrict 0 i ≤ restrict v i
hi₁ : MeasurableSet i
⊢ 0 ≤ ↑v i
[PROOFSTEP]
exact (restrict_le_restrict_iff _ _ hi₁).1 hi₂ hi₁ Set.Subset.rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₂ : restrict 0 i ≤ restrict v i
hi₁ : ¬MeasurableSet i
⊢ 0 ≤ ↑v i
[PROOFSTEP]
rw [v.not_measurable hi₁]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₂ : restrict v i ≤ restrict 0 i
⊢ ↑v i ≤ 0
[PROOFSTEP]
by_cases hi₁ : MeasurableSet i
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₂ : restrict v i ≤ restrict 0 i
hi₁ : MeasurableSet i
⊢ ↑v i ≤ 0
[PROOFSTEP]
exact (restrict_le_restrict_iff _ _ hi₁).1 hi₂ hi₁ Set.Subset.rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₂ : restrict v i ≤ restrict 0 i
hi₁ : ¬MeasurableSet i
⊢ ↑v i ≤ 0
[PROOFSTEP]
rw [v.not_measurable hi₁]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi : ¬MeasurableSet i
⊢ restrict 0 i ≤ restrict v i
[PROOFSTEP]
rw [restrict_zero, restrict_not_measurable _ hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi : ¬MeasurableSet i
⊢ restrict v i ≤ restrict 0 i
[PROOFSTEP]
rw [restrict_zero, restrict_not_measurable _ hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi : ¬restrict v i ≤ restrict 0 i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
[PROOFSTEP]
have hi₁ : MeasurableSet i := measurable_of_not_restrict_le_zero _ hi
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi : ¬restrict v i ≤ restrict 0 i
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
[PROOFSTEP]
rw [restrict_le_restrict_iff _ _ hi₁] at hi 
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑0 j
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
[PROOFSTEP]
push_neg at hi 
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi : Exists fun ⦃j⦄ => MeasurableSet j ∧ j ⊆ i ∧ ↑0 j < ↑v j
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
[PROOFSTEP]
exact hi
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
⊢ v ≪ᵥ w
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
⊢ ↑v s = 0
[PROOFSTEP]
by_cases hmeas : MeasurableSet s
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
hmeas : MeasurableSet s
⊢ ↑v s = 0
[PROOFSTEP]
exact h hmeas hs
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
hmeas : ¬MeasurableSet s
⊢ ↑v s = 0
[PROOFSTEP]
exact not_measurable v hmeas
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ : VectorMeasure α M✝
w✝ : VectorMeasure α N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ -v ≪ᵥ w
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ : VectorMeasure α M✝
w✝ : VectorMeasure α N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(-v) s = 0
[PROOFSTEP]
rw [neg_apply, h hs, neg_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N✝ : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N✝
inst✝³ : TopologicalSpace N✝
v✝ : VectorMeasure α M
w✝ : VectorMeasure α N✝
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : TopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ v ≪ᵥ -w
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N✝ : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N✝
inst✝³ : TopologicalSpace N✝
v✝ : VectorMeasure α M
w✝ : VectorMeasure α N✝
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : TopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑(-w) s = 0
⊢ ↑v s = 0
[PROOFSTEP]
rw [neg_apply, neg_eq_zero] at hs 
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N✝ : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N✝
inst✝³ : TopologicalSpace N✝
v✝ : VectorMeasure α M
w✝ : VectorMeasure α N✝
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : TopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑v s = 0
[PROOFSTEP]
exact h hs
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w✝ : VectorMeasure α N
inst✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
⊢ v₁ + v₂ ≪ᵥ w
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w✝ : VectorMeasure α N
inst✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(v₁ + v₂) s = 0
[PROOFSTEP]
rw [add_apply, hv₁ hs, hv₂ hs, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v : VectorMeasure α M✝
w✝ : VectorMeasure α N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
⊢ v₁ - v₂ ≪ᵥ w
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v : VectorMeasure α M✝
w✝ : VectorMeasure α N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(v₁ - v₂) s = 0
[PROOFSTEP]
rw [sub_apply, hv₁ hs, hv₂ hs, zero_sub, neg_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ : VectorMeasure α M
w✝ : VectorMeasure α N
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ r • v ≪ᵥ w
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ : VectorMeasure α M
w✝ : VectorMeasure α N
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(r • v) s = 0
[PROOFSTEP]
rw [smul_apply, h hs, smul_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
⊢ VectorMeasure.map v f ≪ᵥ VectorMeasure.map w f
[PROOFSTEP]
by_cases hf : Measurable f
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
⊢ VectorMeasure.map v f ≪ᵥ VectorMeasure.map w f
[PROOFSTEP]
refine' mk fun s hs hws => _
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : ↑(VectorMeasure.map w f) s = 0
⊢ ↑(VectorMeasure.map v f) s = 0
[PROOFSTEP]
rw [map_apply _ hf hs] at hws ⊢
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : ↑w (f ⁻¹' s) = 0
⊢ ↑v (f ⁻¹' s) = 0
[PROOFSTEP]
exact h hws
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : ¬Measurable f
⊢ VectorMeasure.map v f ≪ᵥ VectorMeasure.map w f
[PROOFSTEP]
intro s _
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid L
inst✝⁵ : TopologicalSpace L
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
inst✝ : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : ¬Measurable f
s : Set β
a✝ : ↑(VectorMeasure.map w f) s = 0
⊢ ↑(VectorMeasure.map v f) s = 0
[PROOFSTEP]
rw [map_not_measurable v hf, zero_apply]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
⊢ (∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0) ↔ v ≪ᵥ μ
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
⊢ (∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0) → v ≪ᵥ μ
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
⊢ v ≪ᵥ μ → ∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0
⊢ v ≪ᵥ μ
[PROOFSTEP]
refine' mk fun s hmeas hs => h _
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0
s : Set α
hmeas : MeasurableSet s
hs : ↑μ s = 0
⊢ ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
[PROOFSTEP]
rw [← hs, ennrealToMeasure_apply hmeas]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
⊢ ∀ ⦃s : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0 → ↑v s = 0
[PROOFSTEP]
intro s hs
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
⊢ ↑v s = 0
[PROOFSTEP]
by_cases hmeas : MeasurableSet s
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
hmeas : MeasurableSet s
⊢ ↑v s = 0
[PROOFSTEP]
rw [ennrealToMeasure_apply hmeas] at hs 
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑μ s = 0
hmeas : MeasurableSet s
⊢ ↑v s = 0
[PROOFSTEP]
exact h hs
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : ↑↑(VectorMeasure.ennrealToMeasure μ) s = 0
hmeas : ¬MeasurableSet s
⊢ ↑v s = 0
[PROOFSTEP]
exact not_measurable v hmeas
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
⊢ v ⟂ᵥ w
[PROOFSTEP]
refine' ⟨s, hs, fun t hst => _, fun t hst => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ s
⊢ ↑v t = 0
[PROOFSTEP]
by_cases ht : MeasurableSet t
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ sᶜ
⊢ ↑w t = 0
[PROOFSTEP]
by_cases ht : MeasurableSet t
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ s
ht : MeasurableSet t
⊢ ↑v t = 0
[PROOFSTEP]
exact h₁ t hst ht
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ s
ht : ¬MeasurableSet t
⊢ ↑v t = 0
[PROOFSTEP]
exact not_measurable v ht
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ sᶜ
ht : MeasurableSet t
⊢ ↑w t = 0
[PROOFSTEP]
exact h₂ t hst ht
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ sᶜ
ht : ¬MeasurableSet t
⊢ ↑w t = 0
[PROOFSTEP]
exact not_measurable w ht
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
h₁ : v₁ ⟂ᵥ w
h₂ : v₂ ⟂ᵥ w
⊢ v₁ + v₂ ⟂ᵥ w
[PROOFSTEP]
obtain ⟨u, hmu, hu₁, hu₂⟩ := h₁
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
h₂ : v₂ ⟂ᵥ w
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
⊢ v₁ + v₂ ⟂ᵥ w
[PROOFSTEP]
obtain ⟨v, hmv, hv₁, hv₂⟩ := h₂
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
⊢ v₁ + v₂ ⟂ᵥ w
[PROOFSTEP]
refine' mk (u ∩ v) (hmu.inter hmv) (fun t ht _ => _) fun t ht hmt => _
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ u ∩ v
x✝ : MeasurableSet t
⊢ ↑(v₁ + v₂) t = 0
[PROOFSTEP]
rw [add_apply, hu₁ _ (Set.subset_inter_iff.1 ht).1, hv₁ _ (Set.subset_inter_iff.1 ht).2, zero_add]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ (u ∩ v)ᶜ
hmt : MeasurableSet t
⊢ ↑w t = 0
[PROOFSTEP]
rw [Set.compl_inter] at ht 
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ ↑w t = 0
[PROOFSTEP]
rw [(_ : t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t), of_union _ (hmu.compl.inter hmt) ((hmv.compl.diff hmu.compl).inter hmt), hu₂, hv₂,
  add_zero]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.x
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ vᶜ \ uᶜ ∩ t ⊆ vᶜ
[PROOFSTEP]
exact Set.Subset.trans (Set.inter_subset_left _ _) (Set.diff_subset _ _)
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.x
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ uᶜ ∩ t ⊆ uᶜ
[PROOFSTEP]
exact Set.inter_subset_left _ _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ Disjoint (uᶜ ∩ t) (vᶜ \ uᶜ ∩ t)
[PROOFSTEP]
exact disjoint_sdiff_self_right.mono (Set.inter_subset_left _ _) (Set.inter_subset_left _ _)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
[PROOFSTEP]
apply Set.Subset.antisymm
[GOAL]
case h₁
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ t ⊆ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
[PROOFSTEP]
intro x hx
[GOAL]
case h₂
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t ⊆ t
[PROOFSTEP]
intro x hx
[GOAL]
case h₁
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
[PROOFSTEP]
by_cases hxu' : x ∈ uᶜ
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
[PROOFSTEP]
exact Or.inl ⟨hxu', hx⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : ¬x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
[PROOFSTEP]
rcases ht hx with (hxu | hxv)
[GOAL]
case neg.inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : ¬x ∈ uᶜ
hxu : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
case neg.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : ¬x ∈ uᶜ
hxv : x ∈ vᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
[PROOFSTEP]
exacts [False.elim (hxu' hxu), Or.inr ⟨⟨hxv, hxu'⟩, hx⟩]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
⊢ x ∈ t
[PROOFSTEP]
cases' hx with hx hx
[GOAL]
case h₂.inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ uᶜ ∩ t
⊢ x ∈ t
[PROOFSTEP]
exact hx.2
[GOAL]
case h₂.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁷ : AddCommMonoid L
inst✝⁶ : TopologicalSpace L
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ vᶜ \ uᶜ ∩ t
⊢ x ∈ t
[PROOFSTEP]
exact hx.2
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v v₁ v₂ : VectorMeasure α M
w w₁ w₂ : VectorMeasure α N
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R N
inst✝ : ContinuousConstSMul R N
r : R
h : v ⟂ᵥ w
s : Set α
hmeas : MeasurableSet s
hs₁ : ∀ (t : Set α), t ⊆ s → ↑v t = 0
hs₂ : ∀ (t : Set α), t ⊆ sᶜ → ↑w t = 0
t : Set α
ht : t ⊆ sᶜ
⊢ ↑(r • w) t = 0
[PROOFSTEP]
simp only [coe_smul, Pi.smul_apply, hs₂ t ht, smul_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M✝
w✝ w₁ w₂ : VectorMeasure α N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ⟂ᵥ w
⊢ -v ⟂ᵥ w
[PROOFSTEP]
obtain ⟨u, hmu, hu₁, hu₂⟩ := h
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M✝
w✝ w₁ w₂ : VectorMeasure α N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
⊢ -v ⟂ᵥ w
[PROOFSTEP]
refine' ⟨u, hmu, fun s hs => _, hu₂⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M✝
w✝ w₁ w₂ : VectorMeasure α N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
s : Set α
hs : s ⊆ u
⊢ ↑(-v) s = 0
[PROOFSTEP]
rw [neg_apply v s, neg_eq_zero]
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M✝
w✝ w₁ w₂ : VectorMeasure α N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
s : Set α
hs : s ⊆ u
⊢ ↑v s = 0
[PROOFSTEP]
exact hu₁ s hs
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
⊢ (fun i => if MeasurableSet i then ↑v i else 0) ∅ = 0
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
⊢ (if MeasurableSet ∅ then ↑v ∅ else 0) = 0
[PROOFSTEP]
rw [if_pos (@MeasurableSet.empty _ m), v.empty]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : ¬MeasurableSet i
⊢ (fun i => if MeasurableSet i then ↑v i else 0) i = 0
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : ¬MeasurableSet i
⊢ (if MeasurableSet i then ↑v i else 0) = 0
[PROOFSTEP]
rw [if_neg hi]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun i => (fun i => if MeasurableSet i then ↑v i else 0) (f i))
    ((fun i => if MeasurableSet i then ↑v i else 0) (⋃ (i : ℕ), f i))
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun i => if MeasurableSet (f i) then ↑v (f i) else 0)
    (if MeasurableSet (⋃ (i : ℕ), f i) then ↑v (⋃ (i : ℕ), f i) else 0)
[PROOFSTEP]
have hf₁' : ∀ k, MeasurableSet[n] (f k) := fun k => hle _ (hf₁ k)
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
⊢ HasSum (fun i => if MeasurableSet (f i) then ↑v (f i) else 0)
    (if MeasurableSet (⋃ (i : ℕ), f i) then ↑v (⋃ (i : ℕ), f i) else 0)
[PROOFSTEP]
convert v.m_iUnion hf₁' hf₂ using 1
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
⊢ (fun i => if MeasurableSet (f i) then ↑v (f i) else 0) = fun i => ↑v (f i)
[PROOFSTEP]
ext n
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
m n✝ : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n✝
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
n : ℕ
⊢ (if MeasurableSet (f n) then ↑v (f n) else 0) = ↑v (f n)
[PROOFSTEP]
rw [if_pos (hf₁ n)]
[GOAL]
case h.e'_6
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
⊢ (if MeasurableSet (⋃ (i : ℕ), f i) then ↑v (⋃ (i : ℕ), f i) else 0) = ↑v (⋃ (i : ℕ), f i)
[PROOFSTEP]
rw [if_pos (@MeasurableSet.iUnion _ _ m _ _ hf₁)]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
⊢ trim v (_ : n ≤ n) = v
[PROOFSTEP]
ext i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(trim v (_ : n ≤ n)) i = ↑v i
[PROOFSTEP]
exact if_pos hi
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
⊢ trim 0 hle = 0
[PROOFSTEP]
ext i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
⊢ ↑(trim 0 hle) i = ↑0 i
[PROOFSTEP]
exact if_pos hi
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
⊢ restrict (trim v hle) i = trim (restrict v i) hle
[PROOFSTEP]
ext j hj
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict (trim v hle) i) j = ↑(trim (restrict v i) hle) j
[PROOFSTEP]
rw [@restrict_apply _ m, trim_measurableSet_eq hle hj, restrict_apply, trim_measurableSet_eq]
[GOAL]
case h.hi
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet (j ∩ i)
case h.hi
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i
case h.hj
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j
case h.hi
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i
case h.hj
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j
[PROOFSTEP]
all_goals measurability
[GOAL]
case h.hi
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet (j ∩ i)
[PROOFSTEP]
measurability
[GOAL]
case h.hi
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i
[PROOFSTEP]
measurability
[GOAL]
case h.hj
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j
[PROOFSTEP]
measurability
[GOAL]
case h.hi
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i
[PROOFSTEP]
measurability
[GOAL]
case h.hj
α : Type u_1
β : Type u_2
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j
[PROOFSTEP]
measurability
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
j : Set α
hj : MeasurableSet j
⊢ 0 ≤ ↑(VectorMeasure.restrict 0 i) j
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
⊢ Measure α
[PROOFSTEP]
refine' Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi₂) _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
⊢ toMeasureOfZeroLE' s i hi₂ ∅ (_ : MeasurableSet ∅) = 0
[PROOFSTEP]
simp_rw [toMeasureOfZeroLE', s.restrict_apply hi₁ MeasurableSet.empty, Set.empty_inter i, s.empty]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
⊢ ↑{ val := 0, property := (_ : (fun r => 0 ≤ r) 0) } = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
⊢ ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      toMeasureOfZeroLE' s i hi₂ (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) =
        ∑' (i_1 : ℕ), toMeasureOfZeroLE' s i hi₂ (f i_1) (_ : MeasurableSet (f i_1))
[PROOFSTEP]
intro f hf₁ hf₂
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ toMeasureOfZeroLE' s i hi₂ (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) =
    ∑' (i_1 : ℕ), toMeasureOfZeroLE' s i hi₂ (f i_1) (_ : MeasurableSet (f i_1))
[PROOFSTEP]
have h₁ : ∀ n, MeasurableSet (i ∩ f n) := fun n => hi₁.inter (hf₁ n)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
⊢ toMeasureOfZeroLE' s i hi₂ (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) =
    ∑' (i_1 : ℕ), toMeasureOfZeroLE' s i hi₂ (f i_1) (_ : MeasurableSet (f i_1))
[PROOFSTEP]
have h₂ : Pairwise (Disjoint on fun n : ℕ => i ∩ f n) :=
  by
  intro n m hnm
  exact ((hf₂ hnm).inf_left' i).inf_right' i
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
⊢ Pairwise (Disjoint on fun n => i ∩ f n)
[PROOFSTEP]
intro n m hnm
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
n m : ℕ
hnm : n ≠ m
⊢ (Disjoint on fun n => i ∩ f n) n m
[PROOFSTEP]
exact ((hf₂ hnm).inf_left' i).inf_right' i
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (Disjoint on fun n => i ∩ f n)
⊢ toMeasureOfZeroLE' s i hi₂ (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) =
    ∑' (i_1 : ℕ), toMeasureOfZeroLE' s i hi₂ (f i_1) (_ : MeasurableSet (f i_1))
[PROOFSTEP]
simp only [toMeasureOfZeroLE', s.restrict_apply hi₁ (MeasurableSet.iUnion hf₁), Set.inter_comm, Set.inter_iUnion,
  s.of_disjoint_iUnion_nat h₁ h₂, ENNReal.some_eq_coe, id.def]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (Disjoint on fun n => i ∩ f n)
⊢ ↑{ val := ∑' (i_1 : ℕ), ↑s (i ∩ f i_1), property := (_ : (fun r => 0 ≤ r) (∑' (i_1 : ℕ), ↑s (i ∩ f i_1))) } =
    ∑' (i_1 : ℕ),
      ↑{ val := ↑(VectorMeasure.restrict s i) (f i_1), property := (_ : 0 ≤ ↑(VectorMeasure.restrict s i) (f i_1)) }
[PROOFSTEP]
have h : ∀ n, 0 ≤ s (i ∩ f n) := fun n =>
  s.nonneg_of_zero_le_restrict (s.zero_le_restrict_subset hi₁ (Set.inter_subset_left _ _) hi₂)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (Disjoint on fun n => i ∩ f n)
h : ∀ (n : ℕ), 0 ≤ ↑s (i ∩ f n)
⊢ ↑{ val := ∑' (i_1 : ℕ), ↑s (i ∩ f i_1), property := (_ : (fun r => 0 ≤ r) (∑' (i_1 : ℕ), ↑s (i ∩ f i_1))) } =
    ∑' (i_1 : ℕ),
      ↑{ val := ↑(VectorMeasure.restrict s i) (f i_1), property := (_ : 0 ≤ ↑(VectorMeasure.restrict s i) (f i_1)) }
[PROOFSTEP]
rw [NNReal.coe_tsum_of_nonneg h, ENNReal.coe_tsum]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (Disjoint on fun n => i ∩ f n)
h : ∀ (n : ℕ), 0 ≤ ↑s (i ∩ f n)
⊢ ∑' (a : ℕ), ↑{ val := ↑s (i ∩ f a), property := (_ : 0 ≤ ↑s (i ∩ f a)) } =
    ∑' (i_1 : ℕ),
      ↑{ val := ↑(VectorMeasure.restrict s i) (f i_1), property := (_ : 0 ≤ ↑(VectorMeasure.restrict s i) (f i_1)) }
[PROOFSTEP]
refine' tsum_congr fun n => _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (Disjoint on fun n => i ∩ f n)
h : ∀ (n : ℕ), 0 ≤ ↑s (i ∩ f n)
n : ℕ
⊢ ↑{ val := ↑s (i ∩ f n), property := (_ : 0 ≤ ↑s (i ∩ f n)) } =
    ↑{ val := ↑(VectorMeasure.restrict s i) (f n), property := (_ : 0 ≤ ↑(VectorMeasure.restrict s i) (f n)) }
[PROOFSTEP]
simp_rw [s.restrict_apply hi₁ (hf₁ n), Set.inter_comm]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (Disjoint on fun n => i ∩ f n)
h : ∀ (n : ℕ), 0 ≤ ↑s (i ∩ f n)
⊢ Summable fun n => { val := ↑s (i ∩ f n), property := (_ : 0 ≤ ↑s (i ∩ f n)) }
[PROOFSTEP]
exact (NNReal.summable_mk h).2 (s.m_iUnion h₁ h₂).summable
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ ↑↑(toMeasureOfZeroLE s i hi₁ hi) j = ↑{ val := ↑s (i ∩ j), property := (_ : 0 ≤ ↑s (i ∩ j)) }
[PROOFSTEP]
simp_rw [toMeasureOfZeroLE, Measure.ofMeasurable_apply _ hj₁, toMeasureOfZeroLE', s.restrict_apply hi₁ hj₁,
  Set.inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ ↑↑(toMeasureOfLEZero s i hi₁ hi) j = ↑{ val := -↑s (i ∩ j), property := (_ : 0 ≤ -↑s (i ∩ j)) }
[PROOFSTEP]
erw [toMeasureOfZeroLE_apply]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ ↑{ val := ↑(-s) (i ∩ j), property := (_ : 0 ≤ ↑(-s) (i ∩ j)) } =
    ↑{ val := -↑s (i ∩ j), property := (_ : 0 ≤ -↑s (i ∩ j)) }
[PROOFSTEP]
simp
[GOAL]
case hj₁
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ MeasurableSet j
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₁ : MeasurableSet i
⊢ ↑↑(toMeasureOfZeroLE s i hi₁ hi) univ < ⊤
[PROOFSTEP]
rw [toMeasureOfZeroLE_apply s hi hi₁ MeasurableSet.univ]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₁ : MeasurableSet i
⊢ ↑{ val := ↑s (i ∩ univ), property := (_ : 0 ≤ ↑s (i ∩ univ)) } < ⊤
[PROOFSTEP]
exact ENNReal.coe_lt_top
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i
hi₁ : MeasurableSet i
⊢ ↑↑(toMeasureOfLEZero s i hi₁ hi) univ < ⊤
[PROOFSTEP]
rw [toMeasureOfLEZero_apply s hi hi₁ MeasurableSet.univ]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i
hi₁ : MeasurableSet i
⊢ ↑{ val := -↑s (i ∩ univ), property := (_ : 0 ≤ -↑s (i ∩ univ)) } < ⊤
[PROOFSTEP]
exact ENNReal.coe_lt_top
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hs : VectorMeasure.restrict 0 univ ≤ VectorMeasure.restrict s univ
⊢ Measure.toSignedMeasure (toMeasureOfZeroLE s univ (_ : MeasurableSet univ) hs) = s
[PROOFSTEP]
ext i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i✝ j : Set α
hs : VectorMeasure.restrict 0 univ ≤ VectorMeasure.restrict s univ
i : Set α
hi : MeasurableSet i
⊢ ↑(Measure.toSignedMeasure (toMeasureOfZeroLE s univ (_ : MeasurableSet univ) hs)) i = ↑s i
[PROOFSTEP]
simp [hi, toMeasureOfZeroLE_apply _ _ _ hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hs : VectorMeasure.restrict s univ ≤ VectorMeasure.restrict 0 univ
⊢ Measure.toSignedMeasure (toMeasureOfLEZero s univ (_ : MeasurableSet univ) hs) = -s
[PROOFSTEP]
ext i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i✝ j : Set α
hs : VectorMeasure.restrict s univ ≤ VectorMeasure.restrict 0 univ
i : Set α
hi : MeasurableSet i
⊢ ↑(Measure.toSignedMeasure (toMeasureOfLEZero s univ (_ : MeasurableSet univ) hs)) i = ↑(-s) i
[PROOFSTEP]
simp [hi, toMeasureOfLEZero_apply _ _ _ hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ 0 ≤ toSignedMeasure μ
[PROOFSTEP]
rw [← le_restrict_univ_iff_le]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ VectorMeasure.restrict 0 univ ≤ VectorMeasure.restrict (toSignedMeasure μ) univ
[PROOFSTEP]
refine' restrict_le_restrict_of_subset_le _ _ fun j hj₁ _ => _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
j : Set α
hj₁ : MeasurableSet j
x✝ : j ⊆ univ
⊢ ↑0 j ≤ ↑(toSignedMeasure μ) j
[PROOFSTEP]
simp only [Measure.toSignedMeasure_apply_measurable hj₁, coe_zero, Pi.zero_apply, ENNReal.toReal_nonneg,
  VectorMeasure.coe_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ SignedMeasure.toMeasureOfZeroLE (toSignedMeasure μ) univ (_ : MeasurableSet univ)
      (_ : VectorMeasure.restrict 0 univ ≤ VectorMeasure.restrict (toSignedMeasure μ) univ) =
    μ
[PROOFSTEP]
refine' Measure.ext fun i hi => _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
⊢ ↑↑(SignedMeasure.toMeasureOfZeroLE (toSignedMeasure μ) univ (_ : MeasurableSet univ)
            (_ : VectorMeasure.restrict 0 univ ≤ VectorMeasure.restrict (toSignedMeasure μ) univ))
      i =
    ↑↑μ i
[PROOFSTEP]
lift μ i to ℝ≥0 using (measure_lt_top _ _).ne with m hm
[GOAL]
case intro
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = ↑↑μ i
⊢ ↑↑(SignedMeasure.toMeasureOfZeroLE (toSignedMeasure μ) univ (_ : MeasurableSet univ)
            (_ : VectorMeasure.restrict 0 univ ≤ VectorMeasure.restrict (toSignedMeasure μ) univ))
      i =
    ↑m
[PROOFSTEP]
rw [SignedMeasure.toMeasureOfZeroLE_apply _ _ _ hi, coe_eq_coe]
[GOAL]
case intro
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = ↑↑μ i
⊢ { val := ↑(toSignedMeasure μ) (univ ∩ i), property := (_ : 0 ≤ ↑(toSignedMeasure μ) (univ ∩ i)) } = m
[PROOFSTEP]
congr
[GOAL]
case intro.e_val
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = ↑↑μ i
⊢ ↑(toSignedMeasure μ) (univ ∩ i) = ↑m
[PROOFSTEP]
simp [hi, ← hm]
