ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 F<VAR>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>ι : Type u_5<VAR>b : Basis ι 𝕜 E<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<GOAL>A = LinearMap.adjoint B ↔ ∀ (i : ι) (y : F), ⟪A (b i), y⟫_𝕜 = ⟪b i, B y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 F<VAR>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>ι : Type u_5<VAR>b : Basis ι 𝕜 F<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<GOAL>A = LinearMap.adjoint B ↔ ∀ (i : ι) (x : E), ⟪A x, b i⟫_𝕜 = ⟪x, B (b i)⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>A : E →ₗ[𝕜] E<GOAL>star A = LinearMap.adjoint A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>A : E →ₗ[𝕜] E<GOAL>IsSelfAdjoint A ↔ LinearMap.adjoint A = A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>A : E →ₗ[𝕜] E<GOAL>A.IsSymmetric ↔ IsSelfAdjoint A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 F<VAR>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>A : E →ₗ[𝕜] F<GOAL>sesqFormOfInner.IsAdjointPair sesqFormOfInner A (LinearMap.adjoint A)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>T : E →ₗ[𝕜] E<GOAL>(LinearMap.adjoint T * T).IsSymmetric
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>x : E<GOAL>0 ≤ RCLike.re ⟪x, (LinearMap.adjoint T * T) x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>x : E<GOAL>RCLike.im ⟪x, (LinearMap.adjoint T) (T x)⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace 𝕜 H<VAR>CompleteSpace H<VAR>K : Type u_6<VAR>NormedAddCommGroup K<VAR>InnerProductSpace 𝕜 K<VAR>CompleteSpace K<VAR>u : H →L[𝕜] K<GOAL>(∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜) ↔ (ContinuousLinearMap.adjoint u).comp u = 1
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace 𝕜 H<VAR>CompleteSpace H<VAR>K : Type u_6<VAR>NormedAddCommGroup K<VAR>InnerProductSpace 𝕜 K<VAR>CompleteSpace K<VAR>u : H →L[𝕜] K<GOAL>(∀ (x : H), ‖u x‖ = ‖x‖) ↔ (ContinuousLinearMap.adjoint u).comp u = 1
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace 𝕜 H<VAR>CompleteSpace H<VAR>K : Type u_6<VAR>NormedAddCommGroup K<VAR>InnerProductSpace 𝕜 K<VAR>CompleteSpace K<VAR>e : H ≃ₗᵢ[𝕜] K<GOAL>ContinuousLinearMap.adjoint ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace 𝕜 H<VAR>CompleteSpace H<VAR>e : H ≃ₗᵢ[𝕜] H<GOAL>star ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace 𝕜 H<VAR>CompleteSpace H<VAR>u : H →L[𝕜] H<VAR>hu : u ∈ unitary (H →L[𝕜] H)<VAR>x : H<GOAL>‖u x‖ = ‖x‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace 𝕜 H<VAR>CompleteSpace H<VAR>u : H →L[𝕜] H<VAR>hu : u ∈ unitary (H →L[𝕜] H)<VAR>x y : H<GOAL>⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace 𝕜 H<VAR>CompleteSpace H<VAR>u : ↥(unitary (H →L[𝕜] H))<VAR>x : H<GOAL>‖↑u x‖ = ‖x‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace 𝕜 H<VAR>CompleteSpace H<VAR>u : ↥(unitary (H →L[𝕜] H))<VAR>x y : H<GOAL>⟪↑u x, ↑u y⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace 𝕜 H<VAR>CompleteSpace H<VAR>u : ↥(unitary (H →L[𝕜] H))<GOAL>↑{ toLinearEquiv := (unitary.linearIsometryEquiv u).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ↑u
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>InnerProductSpace 𝕜 H<VAR>CompleteSpace H<VAR>e : H ≃ₗᵢ[𝕜] H<GOAL>↑(unitary.linearIsometryEquiv.symm e) = ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 F<VAR>m : Type u_5<VAR>n : Type u_6<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype n<VAR>DecidableEq n<VAR>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>v₁ : OrthonormalBasis n 𝕜 E<VAR>v₂ : OrthonormalBasis m 𝕜 F<VAR>A : Matrix m n 𝕜<GOAL>(Matrix.toLin v₂.toBasis v₁.toBasis) A.conjTranspose = LinearMap.adjoint ((Matrix.toLin v₁.toBasis v₂.toBasis) A)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 E<VAR>InnerProductSpace 𝕜 F<VAR>m : Type u_5<VAR>n : Type u_6<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype n<VAR>DecidableEq n<VAR>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>v₁ : OrthonormalBasis n 𝕜 E<VAR>v₂ : OrthonormalBasis m 𝕜 F<VAR>f : E →ₗ[𝕜] F<GOAL>(LinearMap.toMatrix v₂.toBasis v₁.toBasis) (LinearMap.adjoint f) = ((LinearMap.toMatrix v₁.toBasis v₂.toBasis) f).conjTranspose
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>n : Type u_6<VAR>Fintype n<VAR>DecidableEq n<VAR>FiniteDimensional 𝕜 E<VAR>v₁ : OrthonormalBasis n 𝕜 E<GOAL>∀ (a : E →ₗ[𝕜] E), (LinearMap.toMatrixOrthonormal v₁) a = (↑(LinearMap.toMatrix v₁.toBasis v₁.toBasis)).toFun a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>n : Type u_6<VAR>Fintype n<VAR>DecidableEq n<VAR>FiniteDimensional 𝕜 E<VAR>v₁ : OrthonormalBasis n 𝕜 E<GOAL>∀ (a : Matrix n n 𝕜), (LinearMap.toMatrixOrthonormal v₁).symm a = (LinearMap.toMatrix v₁.toBasis v₁.toBasis).invFun a
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>m : Type u_5<VAR>n : Type u_6<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m n 𝕜<GOAL>Matrix.toEuclideanLin A.conjTranspose = LinearMap.adjoint (Matrix.toEuclideanLin A)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>self : μ.HaveLebesgueDecomposition ν<GOAL>∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>μ.singularPart ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).1 else 0
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>μ.rnDeriv ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ⋯).2 else 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ.HaveLebesgueDecomposition ν<GOAL>Measurable (μ.rnDeriv ν) ∧ μ.singularPart ν ⟂ₘ ν ∧ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : ¬μ.HaveLebesgueDecomposition ν<GOAL>μ.rnDeriv ν = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : ¬μ.HaveLebesgueDecomposition ν<GOAL>μ.singularPart ν = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>Measurable (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>μ.singularPart ν ⟂ₘ ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<GOAL>μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<GOAL>μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<GOAL>ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν = μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>(μ.withDensity f).HaveLebesgueDecomposition μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>μ.singularPart ν ≤ μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>ν.withDensity (μ.rnDeriv ν) ≤ μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_3<GOAL>∀ {x : MeasurableSpace β} {f : α → β}, AEMeasurable f μ → ∀ (ν : MeasureTheory.Measure α), AEMeasurable f (μ.singularPart ν)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_3<GOAL>∀ {x : MeasurableSpace β} {f : α → β}, AEMeasurable f μ → ∀ (ν : MeasureTheory.Measure α), AEMeasurable f (ν.withDensity (μ.rnDeriv ν))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ ⟂ₘ ν<VAR>ν' : MeasureTheory.Measure α<GOAL>μ.singularPart ν' ⟂ₘ ν
<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>h : μ ≪ ν<GOAL>μ.singularPart ν = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.singularPart 0 ν = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.singularPart 0 = μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<GOAL>μ.singularPart ν = 0 ↔ μ ≪ ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<GOAL>ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<GOAL>μ.rnDeriv ν =ᵐ[ν] 0 ↔ μ ⟂ₘ ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.rnDeriv 0 ν =ᵐ[ν] 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>hμν : μ ⟂ₘ ν<GOAL>μ.rnDeriv ν =ᵐ[ν] 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>(ν.withDensity f).singularPart ν = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>(μ.singularPart ν).rnDeriv ν =ᵐ[ν] 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.singularPart μ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>μ.rnDeriv μ =ᵐ[μ] fun x => 1
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<GOAL>μ.singularPart ν = μ ↔ μ ⟂ₘ ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>(μ.singularPart ν).singularPart ν = μ.singularPart ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : μ s ≠ ⊤<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>∫⁻ (x : α), μ.rnDeriv ν x ∂ν < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>MeasureTheory.Integrable (fun x => (μ.rnDeriv ν x).toReal) ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν s : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hs : s ⟂ₘ ν<VAR>hadd : μ = s + ν.withDensity f<GOAL>s = μ.singularPart ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>r : ℝ≥0<GOAL>(r • μ).singularPart ν = r • μ.singularPart ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>μ.singularPart (r • ν) = μ.singularPart ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ₁ μ₂ ν : MeasureTheory.Measure α<VAR>μ₁.HaveLebesgueDecomposition ν<VAR>μ₂.HaveLebesgueDecomposition ν<GOAL>(μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν s : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hs : s ⟂ₘ ν<VAR>hadd : μ = s + ν.withDensity f<GOAL>ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν s : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<VAR>hs : s ⟂ₘ ν<VAR>hadd : μ = s + ν.withDensity f<GOAL>ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν<VAR>s : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<VAR>hs : s ⟂ₘ ν<VAR>hadd : μ = s + ν.withDensity f<GOAL>f =ᵐ[ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν<VAR>s : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hs : s ⟂ₘ ν<VAR>hadd : μ = s + ν.withDensity f<GOAL>f =ᵐ[ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<GOAL>(ν.withDensity f).rnDeriv ν =ᵐ[ν] f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>(ν.withDensity f).rnDeriv ν =ᵐ[ν] f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<VAR>MeasureTheory.SigmaFinite ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.restrict s).rnDeriv ν =ᵐ[ν] s.indicator (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(ν.restrict s).rnDeriv ν =ᵐ[ν] s.indicator 1
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<GOAL>(r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ ⊤<GOAL>(r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ 0<VAR>hr_ne_top : r ≠ ⊤<GOAL>ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν₁ ν₂ μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure ν₁<VAR>MeasureTheory.IsFiniteMeasure ν₂<VAR>ν₁.HaveLebesgueDecomposition μ<VAR>ν₂.HaveLebesgueDecomposition μ<VAR>(ν₁ + ν₂).HaveLebesgueDecomposition μ<GOAL>(ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>h : ¬μ ⟂ₘ ν<GOAL>∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ MeasureTheory.VectorMeasure.restrict 0 E ≤ MeasureTheory.VectorMeasure.restrict (μ.toSignedMeasure - (ε • ν).toSignedMeasure) E
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>0 ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : f ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν<VAR>hg : g ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν<GOAL>(fun a => f a ⊔ g a) ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν
<VAR>α : Sort u_3<VAR>f : ℕ → α → ℝ≥0∞<VAR>m : ℕ<VAR>a : α<GOAL>⨆ k, ⨆ (_ : k ≤ m + 1), f k a = f m.succ a ⊔ ⨆ k, ⨆ (_ : k ≤ m), f k a
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), f n ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν<VAR>n : ℕ<GOAL>(fun x => ⨆ k, ⨆ (_ : k ≤ n), f k x) ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), f n ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν<VAR>n : ℕ<GOAL>⨆ k, ⨆ (_ : k ≤ n), f k ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν
<VAR>α : Type u_3<VAR>f : ℕ → α → ℝ≥0∞<GOAL>Monotone fun n x => ⨆ k, ⨆ (_ : k ≤ n), f k x
<VAR>α : Type u_3<VAR>f : ℕ → α → ℝ≥0∞<VAR>x : α<GOAL>Monotone fun n => ⨆ k, ⨆ (_ : k ≤ n), f k x
<VAR>α : Type u_3<VAR>f : ℕ → α → ℝ≥0∞<VAR>n k : ℕ<VAR>hk : k ≤ n<GOAL>f k ≤ fun x => ⨆ k, ⨆ (_ : k ≤ n), f k x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure ν<GOAL>μ.HaveLebesgueDecomposition ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>_h : ∀ (μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ], μ.HaveLebesgueDecomposition ν<GOAL>μ.HaveLebesgueDecomposition ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν<VAR>MeasureTheory.SigmaFinite μ<VAR>r : ℝ≥0<GOAL>(r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν<VAR>MeasureTheory.SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ ⊤<GOAL>(r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν<VAR>MeasureTheory.SigmaFinite μ<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν<VAR>MeasureTheory.SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ 0<VAR>hr_ne_top : r ≠ ⊤<GOAL>ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ν₁ ν₂ μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite ν₁<VAR>MeasureTheory.SigmaFinite ν₂<VAR>MeasureTheory.SigmaFinite μ<GOAL>(ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.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>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>CompleteSpace A<VAR>a : A<VAR>IsStarNormal a<GOAL>spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>CompleteSpace A<VAR>a : A<VAR>IsStarNormal a<VAR>h : IsUnit a<GOAL>IsUnit ⟨a, ⋯⟩
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>CompleteSpace A<VAR>S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : A<VAR>h : IsUnit x<VAR>hxS : x ∈ S<GOAL>↑h.unit⁻¹ ∈ S
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>CompleteSpace A<VAR>S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : ↥S<GOAL>IsUnit ↑x ↔ IsUnit x
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>CompleteSpace A<VAR>S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : ↥S<VAR>z : ℂ<GOAL>z ∈ spectrum ℂ x ↔ z ∈ spectrum ℂ ↑x
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>CompleteSpace A<VAR>S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : ↥S<GOAL>spectrum ℂ x = spectrum ℂ ↑x
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>CompleteSpace A<VAR>x : A<VAR>φ : ↑(WeakDual.characterSpace ℂ ↥(elementalStarAlgebra ℂ x))<GOAL>↑(elementalStarAlgebra.characterSpaceToSpectrum x φ) = φ ⟨x, ⋯⟩
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>CompleteSpace A<VAR>x : A<GOAL>Continuous (elementalStarAlgebra.characterSpaceToSpectrum x)
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>CompleteSpace A<VAR>a : A<VAR>IsStarNormal a<GOAL>Function.Bijective (elementalStarAlgebra.characterSpaceToSpectrum a)
<VAR>A : Type u_1<VAR>NormedRing A<VAR>NormedAlgebra ℂ A<VAR>StarRing A<VAR>CstarRing A<VAR>StarModule ℂ A<VAR>CompleteSpace A<VAR>a : A<VAR>IsStarNormal a<GOAL>(continuousFunctionalCalculus a) (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) = ⟨a, ⋯⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>(convexHull 𝕜).IsClosed s = Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>s ⊆ (convexHull 𝕜) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>Convex 𝕜 ((convexHull 𝕜) s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>(convexHull 𝕜) s = ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : Convex 𝕜 t), t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<GOAL>x ∈ (convexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<GOAL>s ⊆ t → Convex 𝕜 t → (convexHull 𝕜) s ⊆ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>ht : Convex 𝕜 t<GOAL>(convexHull 𝕜) s ⊆ t ↔ s ⊆ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>hst : s ⊆ t<GOAL>(convexHull 𝕜) s ⊆ (convexHull 𝕜) t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>(convexHull 𝕜) s = s ↔ Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<GOAL>(convexHull 𝕜) Set.univ = Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<GOAL>(convexHull 𝕜) ∅ = ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>(convexHull 𝕜) s = ∅ ↔ s = ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>((convexHull 𝕜) s).Nonempty ↔ s.Nonempty
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>segment 𝕜 x y ⊆ (convexHull 𝕜) s