ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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<VAR>hi₂ : v.restrict i ≤ w.restrict i<VAR>j : Set α<VAR>hj : j ⊆ i<GOAL>↑v j ≤ ↑w j
<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>h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑w j<GOAL>v.restrict i ≤ w.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<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : v.restrict i ≤ w.restrict i<VAR>hij : j ⊆ i<GOAL>v.restrict j ≤ w.restrict j
<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.restrict ∅ ≤ w.restrict ∅
<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.restrict Set.univ ≤ w.restrict Set.univ ↔ v ≤ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommGroup M<VAR>TopologicalAddGroup M<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>h : v.restrict i ≤ w.restrict i<GOAL>(-w).restrict i ≤ (-v).restrict i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommGroup M<VAR>TopologicalAddGroup M<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>(-w).restrict i ≤ (-v).restrict i ↔ v.restrict i ≤ w.restrict i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>OrderClosedTopology M<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), v.restrict (f n) ≤ w.restrict (f n)<GOAL>v.restrict (⋃ n, f n) ≤ w.restrict (⋃ n, f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>OrderClosedTopology M<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>Countable β<VAR>f : β → Set α<VAR>hf₁ : ∀ (b : β), MeasurableSet (f b)<VAR>hf₂ : ∀ (b : β), v.restrict (f b) ≤ w.restrict (f b)<GOAL>v.restrict (⋃ b, f b) ≤ w.restrict (⋃ b, f b)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>OrderClosedTopology M<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : v.restrict i ≤ w.restrict i<VAR>hj₁ : MeasurableSet j<VAR>hj₂ : v.restrict j ≤ w.restrict j<GOAL>v.restrict (i ∪ j) ≤ w.restrict (i ∪ j)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi₂ : MeasureTheory.VectorMeasure.restrict 0 i ≤ v.restrict i<GOAL>0 ≤ ↑v i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi₂ : v.restrict i ≤ MeasureTheory.VectorMeasure.restrict 0 i<GOAL>↑v i ≤ 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : ¬MeasurableSet i<GOAL>MeasureTheory.VectorMeasure.restrict 0 i ≤ v.restrict i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : ¬MeasurableSet i<GOAL>v.restrict i ≤ MeasureTheory.VectorMeasure.restrict 0 i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : ¬MeasureTheory.VectorMeasure.restrict 0 i ≤ v.restrict i<GOAL>MeasurableSet i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : ¬v.restrict i ≤ MeasureTheory.VectorMeasure.restrict 0 i<GOAL>MeasurableSet i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hij : j ⊆ i<VAR>hi₂ : MeasureTheory.VectorMeasure.restrict 0 i ≤ v.restrict i<GOAL>MeasureTheory.VectorMeasure.restrict 0 j ≤ v.restrict j
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>OrderedAddCommMonoid M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i j : Set α<VAR>hi₁ : MeasurableSet i<VAR>hij : j ⊆ i<VAR>hi₂ : v.restrict i ≤ MeasureTheory.VectorMeasure.restrict 0 i<GOAL>v.restrict j ≤ MeasureTheory.VectorMeasure.restrict 0 j
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>LinearOrderedAddCommMonoid M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>i : Set α<VAR>hi : ¬v.restrict i ≤ MeasureTheory.VectorMeasure.restrict 0 i<GOAL>∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0<GOAL>v ≪ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v w : MeasureTheory.VectorMeasure α M<VAR>h : v = w<GOAL>v ≪ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>v ≪ᵥ v
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid L<VAR>TopologicalSpace L<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>u : MeasureTheory.VectorMeasure α L<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>huv : u ≪ᵥ v<VAR>hvw : v ≪ᵥ w<GOAL>u ≪ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>v : MeasureTheory.VectorMeasure α N<GOAL>0 ≪ᵥ v
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>N : Type u_5<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>M : Type u_6<VAR>AddCommGroup M<VAR>TopologicalSpace M<VAR>TopologicalAddGroup M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>h : v ≪ᵥ w<GOAL>-v ≪ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>N : Type u_6<VAR>AddCommGroup N<VAR>TopologicalSpace N<VAR>TopologicalAddGroup N<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>h : v ≪ᵥ w<GOAL>v ≪ᵥ -w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>ContinuousAdd M<VAR>v₁ v₂ : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>hv₁ : v₁ ≪ᵥ w<VAR>hv₂ : v₂ ≪ᵥ w<GOAL>v₁ + v₂ ≪ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>N : Type u_5<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>M : Type u_6<VAR>AddCommGroup M<VAR>TopologicalSpace M<VAR>TopologicalAddGroup M<VAR>v₁ v₂ : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>hv₁ : v₁ ≪ᵥ w<VAR>hv₂ : v₂ ≪ᵥ w<GOAL>v₁ - v₂ ≪ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>R : Type u_6<VAR>Semiring R<VAR>DistribMulAction R M<VAR>ContinuousConstSMul R M<VAR>r : R<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>h : v ≪ᵥ w<GOAL>r • v ≪ᵥ w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>MeasureTheory.MeasureSpace β<VAR>h : v ≪ᵥ w<VAR>f : α → β<GOAL>v.map f ≪ᵥ w.map f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>μ : MeasureTheory.VectorMeasure α ℝ≥0∞<GOAL>(∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0 → ↑v s = 0) ↔ v ≪ᵥ μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h₁ : ∀ t ⊆ s, MeasurableSet t → ↑v t = 0<VAR>h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → ↑w t = 0<GOAL>v ⟂ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>h : v ⟂ᵥ w<GOAL>w ⟂ᵥ v
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>v ⟂ᵥ 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>w : MeasureTheory.VectorMeasure α N<GOAL>0 ⟂ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>v₁ v₂ : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>T2Space N<VAR>ContinuousAdd M<VAR>h₁ : v₁ ⟂ᵥ w<VAR>h₂ : v₂ ⟂ᵥ w<GOAL>v₁ + v₂ ⟂ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w₁ w₂ : MeasureTheory.VectorMeasure α N<VAR>T2Space M<VAR>ContinuousAdd N<VAR>h₁ : v ⟂ᵥ w₁<VAR>h₂ : v ⟂ᵥ w₂<GOAL>v ⟂ᵥ w₁ + w₂
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>R : Type u_6<VAR>Semiring R<VAR>DistribMulAction R N<VAR>ContinuousConstSMul R N<VAR>r : R<VAR>h : v ⟂ᵥ w<GOAL>v ⟂ᵥ r • w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>R : Type u_6<VAR>Semiring R<VAR>DistribMulAction R M<VAR>ContinuousConstSMul R M<VAR>r : R<VAR>h : v ⟂ᵥ w<GOAL>r • v ⟂ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>N : Type u_5<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>M : Type u_6<VAR>AddCommGroup M<VAR>TopologicalSpace M<VAR>TopologicalAddGroup M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>h : v ⟂ᵥ w<GOAL>-v ⟂ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>N : Type u_6<VAR>AddCommGroup N<VAR>TopologicalSpace N<VAR>TopologicalAddGroup N<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<VAR>h : v ⟂ᵥ w<GOAL>v ⟂ᵥ -w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>N : Type u_5<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>M : Type u_6<VAR>AddCommGroup M<VAR>TopologicalSpace M<VAR>TopologicalAddGroup M<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<GOAL>-v ⟂ᵥ w ↔ v ⟂ᵥ w
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>N : Type u_6<VAR>AddCommGroup N<VAR>TopologicalSpace N<VAR>TopologicalAddGroup N<VAR>v : MeasureTheory.VectorMeasure α M<VAR>w : MeasureTheory.VectorMeasure α N<GOAL>v ⟂ᵥ -w ↔ v ⟂ᵥ w
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>m n : MeasurableSpace α<VAR>v : MeasureTheory.VectorMeasure α M<VAR>hle : m ≤ n<VAR>i : Set α<GOAL>↑(v.trim hle) i = if MeasurableSet i then ↑v i else 0
<VAR>α : Type u_1<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>n : MeasurableSpace α<VAR>v : MeasureTheory.VectorMeasure α M<GOAL>v.trim ⋯ = v
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>n : MeasurableSpace α<VAR>hle : m ≤ n<GOAL>MeasureTheory.VectorMeasure.trim 0 hle = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>n : MeasurableSpace α<VAR>v : MeasureTheory.VectorMeasure α M<VAR>hle : m ≤ n<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(v.trim hle) i = ↑v i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>n : MeasurableSpace α<VAR>v : MeasureTheory.VectorMeasure α M<VAR>hle : m ≤ n<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>(v.trim hle).restrict i = (v.restrict i).trim hle
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i j : Set α<VAR>hi : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i<VAR>hi₁ : MeasurableSet i<VAR>hj₁ : MeasurableSet j<GOAL>(s.toMeasureOfZeroLE i hi₁ hi) j = ↑⟨↑s (i ∩ j), ⋯⟩
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i j : Set α<VAR>hi : MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i<VAR>hi₁ : MeasurableSet i<VAR>hj₁ : MeasurableSet j<GOAL>(s.toMeasureOfLEZero i hi₁ hi) j = ↑⟨-↑s (i ∩ j), ⋯⟩
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>hs : MeasureTheory.VectorMeasure.restrict 0 Set.univ ≤ MeasureTheory.VectorMeasure.restrict s Set.univ<GOAL>(s.toMeasureOfZeroLE Set.univ ⋯ hs).toSignedMeasure = s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>hs : MeasureTheory.VectorMeasure.restrict s Set.univ ≤ MeasureTheory.VectorMeasure.restrict 0 Set.univ<GOAL>(s.toMeasureOfLEZero Set.univ ⋯ hs).toSignedMeasure = -s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>0 ≤ μ.toSignedMeasure
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>μ.toSignedMeasure.toMeasureOfZeroLE Set.univ ⋯ ⋯ = μ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<VAR>x : E<GOAL>(f.fpowerSeries x).radius = ⊤
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<VAR>x : E<GOAL>HasFPowerSeriesOnBall (⇑f) (f.fpowerSeries x) x ⊤
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<VAR>x : E<GOAL>HasFPowerSeriesAt (⇑f) (f.fpowerSeries x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<VAR>x : E<GOAL>AnalyticAt 𝕜 (⇑f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>m : Fin 2 → E × F<GOAL>f.uncurryBilinear m = (f (m 0).1) (m 1).2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>x : E × F<GOAL>f.fpowerSeriesBilinear x 0 = ContinuousMultilinearMap.curry0 𝕜 (E × F) ((f x.1) x.2)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>x : E × F<GOAL>f.fpowerSeriesBilinear x 1 = (continuousMultilinearCurryFin1 𝕜 (E × F) G).symm (f.deriv₂ x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>x : E × F<GOAL>f.fpowerSeriesBilinear x 2 = f.uncurryBilinear
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>x : E × F<VAR>n : ℕ<GOAL>f.fpowerSeriesBilinear x (n + 3) = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>x : E × F<GOAL>(f.fpowerSeriesBilinear x).radius = ⊤
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>x : E × F<GOAL>HasFPowerSeriesOnBall (fun x => (f x.1) x.2) (f.fpowerSeriesBilinear x) x ⊤
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>x : E × F<GOAL>HasFPowerSeriesAt (fun x => (f x.1) x.2) (f.fpowerSeriesBilinear x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>x : E × F<GOAL>AnalyticAt 𝕜 (fun x => (f x.1) x.2) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>z : E<GOAL>AnalyticAt 𝕜 id z
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<GOAL>AnalyticOn 𝕜 (fun x => x) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : E × F<GOAL>AnalyticAt 𝕜 (fun p => p.1) p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : E × F<GOAL>AnalyticAt 𝕜 (fun p => p.2) p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set (E × F)<GOAL>AnalyticOn 𝕜 (fun p => p.1) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set (E × F)<GOAL>AnalyticOn 𝕜 (fun p => p.2) s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<VAR>h : μ ≪ ν<GOAL>ν.withDensity (μ.rnDeriv ν) = μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<GOAL>μ ≪ ν ↔ ν.withDensity (μ.rnDeriv ν) = μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<GOAL>∀ᵐ (x : α) ∂μ, 0 < μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SFinite ν<VAR>hμν : μ ≪ ν<GOAL>∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<GOAL>(ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hf : AEMeasurable f ν<GOAL>(μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x => f x * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>(μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x => f x * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<GOAL>μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun x => (f x)⁻¹ * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<GOAL>μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun x => (f x)⁻¹ * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>ν' : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν'<VAR>h : μ ⟂ₘ ν<VAR>hνν' : ν ≪ ν'<GOAL>μ.rnDeriv ν' =ᵐ[ν] 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν ν' : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>MeasureTheory.SigmaFinite ν'<VAR>hμν : μ ≪ ν<VAR>hνν' : ν ⟂ₘ ν'<GOAL>μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν ν' : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>MeasureTheory.SigmaFinite ν'<VAR>hμν' : μ ⟂ₘ ν'<VAR>hνν' : ν ⟂ₘ ν'<GOAL>μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν ν' : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>MeasureTheory.SigmaFinite ν'<VAR>hνν' : ν ⟂ₘ ν'<GOAL>μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᵐ[μ] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hνμ : ν ≪ μ<GOAL>(μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ