ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<GOAL>s ⟂ᵥ t ↔ s.totalVariation ⟂ₘ t.totalVariation
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.VectorMeasure α ℝ≥0∞<GOAL>s ⟂ᵥ μ ↔ s.totalVariation ⟂ₘ μ.ennrealToMeasure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<GOAL>s.totalVariation ⟂ₘ μ ↔ s.toJordanDecomposition.posPart ⟂ₘ μ ∧ s.toJordanDecomposition.negPart ⟂ₘ μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>self : s.HaveLebesgueDecomposition μ<GOAL>s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>self : s.HaveLebesgueDecomposition μ<GOAL>s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<GOAL>¬s.HaveLebesgueDecomposition μ ↔ ¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ ∨ ¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<GOAL>s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<GOAL>(s.singularPart μ).totalVariation = s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<GOAL>s.singularPart μ ⟂ᵥ μ.toENNRealVectorMeasure
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<GOAL>s.rnDeriv μ = fun x => (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<GOAL>Measurable (s.rnDeriv μ)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Integrable (s.rnDeriv μ) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : MeasureTheory.SignedMeasure α<VAR>s.HaveLebesgueDecomposition μ<GOAL>s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : MeasureTheory.SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<GOAL>(t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)) ⟂ₘ t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : MeasureTheory.SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : MeasureTheory.Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<GOAL>s.toJordanDecomposition = MeasureTheory.JordanDecomposition.mk (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)) (t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)) ⋯
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : MeasureTheory.Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<GOAL>s.HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<GOAL>s.HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : MeasureTheory.SignedMeasure α<VAR>t : MeasureTheory.SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>hfi : MeasureTheory.Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<GOAL>t = s.singularPart μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : MeasureTheory.SignedMeasure α<VAR>t : MeasureTheory.SignedMeasure α<VAR>f : α → ℝ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<GOAL>t = s.singularPart μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.SignedMeasure.singularPart 0 μ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<GOAL>(-s).singularPart μ = -s.singularPart μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0<GOAL>(r • s).singularPart μ = r • s.singularPart μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ<GOAL>(r • s).singularPart μ = r • s.singularPart μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>s.HaveLebesgueDecomposition μ<VAR>t.HaveLebesgueDecomposition μ<GOAL>(s + t).singularPart μ = s.singularPart μ + t.singularPart μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>s.HaveLebesgueDecomposition μ<VAR>t.HaveLebesgueDecomposition μ<GOAL>(s - t).singularPart μ = s.singularPart μ - t.singularPart μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : MeasureTheory.SignedMeasure α<VAR>t : MeasureTheory.SignedMeasure α<VAR>f : α → ℝ<VAR>hfi : MeasureTheory.Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<GOAL>f =ᵐ[μ] s.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>s.HaveLebesgueDecomposition μ<GOAL>(-s).rnDeriv μ =ᵐ[μ] -s.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>s.HaveLebesgueDecomposition μ<VAR>r : ℝ<GOAL>(r • s).rnDeriv μ =ᵐ[μ] r • s.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>s.HaveLebesgueDecomposition μ<VAR>t.HaveLebesgueDecomposition μ<VAR>(s + t).HaveLebesgueDecomposition μ<GOAL>(s + t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ + t.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>s.HaveLebesgueDecomposition μ<VAR>t.HaveLebesgueDecomposition μ<VAR>hst : (s - t).HaveLebesgueDecomposition μ<GOAL>(s - t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ - t.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>c : MeasureTheory.ComplexMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>self : c.HaveLebesgueDecomposition μ<GOAL>(MeasureTheory.ComplexMeasure.im c).HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>c : MeasureTheory.ComplexMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>self : c.HaveLebesgueDecomposition μ<GOAL>(MeasureTheory.ComplexMeasure.re c).HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>c : MeasureTheory.ComplexMeasure α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Integrable (c.rnDeriv μ) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : MeasureTheory.ComplexMeasure α<VAR>c.HaveLebesgueDecomposition μ<GOAL>c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>self : MeasureTheory.VectorMeasure α M<VAR>f : ℕ → Set α<GOAL>(∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → HasSum (fun i => ↑self (f i)) (↑self (⋃ i, f i))
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>self : MeasureTheory.VectorMeasure α M<VAR>i : Set α<GOAL>¬MeasurableSet i → ↑self i = 0
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>self : MeasureTheory.VectorMeasure α M<GOAL>↑self ∅ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>↑v ∅ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : ¬MeasurableSet i<GOAL>↑v i = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>↑v (⋃ i, f i) = ∑' (i : ℕ), ↑v (f i)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<GOAL>Function.Injective MeasureTheory.VectorMeasure.measureOf'
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v w : MeasureTheory.VectorMeasure α M<GOAL>v = w ↔ ∀ (i : Set α), ↑v i = ↑w i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v w : MeasureTheory.VectorMeasure α M<GOAL>v = w ↔ ∀ (i : Set α), MeasurableSet i → ↑v i = ↑w i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>s t : MeasureTheory.VectorMeasure α M<VAR>h : ∀ (i : Set α), MeasurableSet i → ↑s i = ↑t i<GOAL>s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (i : β), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>↑v (⋃ i, f i) = ∑' (i : β), ↑v (f i)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>A B : Set α<VAR>h : Disjoint A B<VAR>hA : MeasurableSet A<VAR>hB : MeasurableSet B<GOAL>↑v (A ∪ B) = ↑v A + ↑v B
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>A B : Set α<VAR>hA : MeasurableSet A<VAR>hB : MeasurableSet B<VAR>h : A ⊆ B<GOAL>↑v A + ↑v (B \ A) = ↑v B
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>A B : Set α<VAR>hA : MeasurableSet A<VAR>hB : MeasurableSet B<VAR>h : A ⊆ B<GOAL>↑v (B \ A) = ↑v B - ↑v A
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>A B : Set α<VAR>hA : MeasurableSet A<VAR>hB : MeasurableSet B<VAR>h' : ↑v (B \ A) = 0<GOAL>↑v (A \ B) + ↑v B = ↑v A
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : ℕ → Set α<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>OrderClosedTopology M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>hf₃ : ∀ (i : ℕ), 0 ≤ ↑v (f i)<GOAL>0 ≤ ↑v (⋃ i, f i)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : ℕ → Set α<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>OrderClosedTopology M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<VAR>hf₃ : ∀ (i : ℕ), ↑v (f i) ≤ 0<GOAL>↑v (⋃ i, f i) ≤ 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>A B : Set α<VAR>h : Disjoint A B<VAR>hA₁ : MeasurableSet A<VAR>hB₁ : MeasurableSet B<VAR>hA₂ : 0 ≤ ↑s A<VAR>hB₂ : 0 ≤ ↑s B<VAR>hAB : ↑s (A ∪ B) = 0<GOAL>↑s A = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>A B : Set α<VAR>h : Disjoint A B<VAR>hA₁ : MeasurableSet A<VAR>hB₁ : MeasurableSet B<VAR>hA₂ : ↑s A ≤ 0<VAR>hB₂ : ↑s B ≤ 0<VAR>hAB : ↑s (A ∪ B) = 0<GOAL>↑s A = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>R : Type u_4<VAR>Semiring R<VAR>DistribMulAction R M<VAR>ContinuousConstSMul R M<VAR>r : R<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>↑(r • v) = r • ↑v
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>R : Type u_4<VAR>Semiring R<VAR>DistribMulAction R M<VAR>ContinuousConstSMul R M<VAR>r : R<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<GOAL>↑(r • v) i = r • ↑v i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>i : Set α<GOAL>↑0 i = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>v w : MeasureTheory.VectorMeasure α M<GOAL>↑(v + w) = ↑v + ↑w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>i : Set α<GOAL>↑(v + w) i = ↑v i + ↑w i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>self : MeasureTheory.VectorMeasure α M<GOAL>∀ (a : Set α), MeasureTheory.VectorMeasure.coeFnAddMonoidHom self a = ↑self a
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>TopologicalSpace M<VAR>TopologicalAddGroup M<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>↑(-v) = -↑v
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>TopologicalSpace M<VAR>TopologicalAddGroup M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<GOAL>↑(-v) i = -↑v i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>TopologicalSpace M<VAR>TopologicalAddGroup M<VAR>v w : MeasureTheory.VectorMeasure α M<GOAL>↑(v - w) = ↑v - ↑w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>TopologicalSpace M<VAR>TopologicalAddGroup M<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>i : Set α<GOAL>↑(v - w) i = ↑v i - ↑w i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hμ : MeasureTheory.IsFiniteMeasure μ<VAR>s : Set α<GOAL>↑μ.toSignedMeasure s = if MeasurableSet s then (μ s).toReal else 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑μ.toSignedMeasure i = (μ i).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>h : μ = ν<GOAL>μ.toSignedMeasure = ν.toSignedMeasure
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure ν<GOAL>μ.toSignedMeasure = ν.toSignedMeasure ↔ μ = ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<GOAL>MeasureTheory.Measure.toSignedMeasure 0 = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure ν<GOAL>(μ + ν).toSignedMeasure = μ.toSignedMeasure + ν.toSignedMeasure
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>r : ℝ≥0<GOAL>(r • μ).toSignedMeasure = r • μ.toSignedMeasure
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>i : Set α<GOAL>↑μ.toENNRealVectorMeasure i = if MeasurableSet i then μ i else 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑μ.toENNRealVectorMeasure i = μ i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<GOAL>MeasureTheory.Measure.toENNRealVectorMeasure 0 = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>(μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(μ.toSignedMeasure - ν.toSignedMeasure) i = (μ i).toReal - (ν i).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>v : MeasureTheory.VectorMeasure α ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>v.ennrealToMeasure s = ↑v s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.VectorMeasure α ℝ≥0∞<GOAL>μ.ennrealToMeasure.toENNRealVectorMeasure = μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.toENNRealVectorMeasure.ennrealToMeasure = μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.VectorMeasure.equivMeasure.symm μ = μ.toENNRealVectorMeasure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>v : MeasureTheory.VectorMeasure α ℝ≥0∞<GOAL>MeasureTheory.VectorMeasure.equivMeasure v = v.ennrealToMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>f : α → β<VAR>hf : ¬Measurable f<GOAL>v.map f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>f : α → β<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>↑(v.map f) s = ↑v (f ⁻¹' s)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>v.map id = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>f : α → β<GOAL>MeasureTheory.VectorMeasure.map 0 f = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>N : Type u_4<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>f : M →+ N<VAR>hf : Continuous ⇑f<VAR>s : Set α<GOAL>↑(v.mapRange f hf) s = f (↑v s)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>v.mapRange (AddMonoidHom.id M) ⋯ = v
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>N : Type u_4<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>f : M →+ N<VAR>hf : Continuous ⇑f<GOAL>MeasureTheory.VectorMeasure.mapRange 0 f hf = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>N : Type u_4<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>ContinuousAdd M<VAR>ContinuousAdd N<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>f : M →+ N<VAR>hf : Continuous ⇑f<GOAL>(v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : ¬MeasurableSet i<GOAL>v.restrict i = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>j : Set α<VAR>hj : MeasurableSet j<GOAL>↑(v.restrict i) j = ↑v (j ∩ i)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>j : Set α<VAR>hj : MeasurableSet j<VAR>hij : j ⊆ i<GOAL>↑(v.restrict i) j = ↑v j
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>v.restrict ∅ = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>v.restrict Set.univ = v
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>i : Set α<GOAL>MeasureTheory.VectorMeasure.restrict 0 i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>f : α → β<GOAL>(v + w).map f = v.map f + w.map f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>f : α → β<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>(MeasureTheory.VectorMeasure.mapGm f) v = v.map f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>i : Set α<GOAL>(v + w).restrict i = v.restrict i + w.restrict i
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>i : Set α<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>(MeasureTheory.VectorMeasure.restrictGm i) v = v.restrict i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>MeasurableSpace β<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>R : Type u_4<VAR>Semiring R<VAR>DistribMulAction R M<VAR>ContinuousConstSMul R M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>f : α → β<VAR>c : R<GOAL>(c • v).map f = c • v.map f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>R : Type u_4<VAR>Semiring R<VAR>DistribMulAction R M<VAR>ContinuousConstSMul R M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>c : R<GOAL>(c • v).restrict i = c • v.restrict i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>MeasurableSpace β<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>R : Type u_4<VAR>Semiring R<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M<VAR>f : α → β<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>(MeasureTheory.VectorMeasure.mapₗ f) v = v.map f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>R : Type u_4<VAR>Semiring R<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M<VAR>i : Set α<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>(MeasureTheory.VectorMeasure.restrictₗ i) v = v.restrict i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>PartialOrder M<VAR>v w : MeasureTheory.VectorMeasure α M<GOAL>v ≤ w ↔ ∀ (i : Set α), MeasurableSet i → ↑v i ≤ ↑w i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>PartialOrder M<VAR>v w : MeasureTheory.VectorMeasure α M<GOAL>v ≤ w ↔ ∀ (i : Set α), ↑v i ≤ ↑w i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>AddCommMonoid M<VAR>PartialOrder M<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>v.restrict i ≤ w.restrict i ↔ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑w j