ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>GaloisConnection Submodule.orthogonal Submodule.orthogonal
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K₁ K₂ : Submodule 𝕜 E<VAR>h : K₁ ≤ K₂<GOAL>K₂ᗮ ≤ K₁ᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K₁ K₂ : Submodule 𝕜 E<VAR>h : K₁ ≤ K₂<GOAL>K₁ᗮᗮ ≤ K₂ᗮᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>K ≤ Kᗮᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K₁ K₂ : Submodule 𝕜 E<GOAL>K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>K : ι → Submodule 𝕜 E<GOAL>⨅ i, (K i)ᗮ = (iSup K)ᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>s : Set (Submodule 𝕜 E)<GOAL>⨅ K ∈ s, Kᗮ = (sSup s)ᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>⊤ᗮ = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>⊥ᗮ = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>Kᗮ = ⊤ ↔ K = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>OrthogonalFamily 𝕜 (fun b => ↥(bif b then K else Kᗮ)) fun b => (bif b then K else Kᗮ).subtypeₗᵢ
<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>K : Submodule ℝ E<GOAL>K.orthogonalBilin bilinFormOfRealInner = Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V : Submodule 𝕜 E<GOAL>U ⟂ V ↔ U ≤ Vᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V : Submodule 𝕜 E<VAR>h : U ⟂ V<GOAL>V ⟂ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V : Submodule 𝕜 E<GOAL>U ⟂ V ↔ V ⟂ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<GOAL>Symmetric Submodule.IsOrtho
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V : Submodule 𝕜 E<VAR>h : U ⟂ V<VAR>u v : E<VAR>hu : u ∈ U<VAR>hv : v ∈ V<GOAL>⟪u, v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V : Submodule 𝕜 E<GOAL>U ⟂ V ↔ ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>V : Submodule 𝕜 E<GOAL>⊥ ⟂ V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U : Submodule 𝕜 E<GOAL>U ⟂ ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U₁ U₂ V : Submodule 𝕜 E<VAR>hU : U₂ ≤ U₁<VAR>h : U₁ ⟂ V<GOAL>U₂ ⟂ V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V₁ V₂ : Submodule 𝕜 E<VAR>hV : V₂ ≤ V₁<VAR>h : U ⟂ V₁<GOAL>U ⟂ V₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U₁ V₁ U₂ V₂ : Submodule 𝕜 E<VAR>hU : U₂ ≤ U₁<VAR>hV : V₂ ≤ V₁<VAR>h : U₁ ⟂ V₁<GOAL>U₂ ⟂ V₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U : Submodule 𝕜 E<GOAL>U ⟂ U ↔ U = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U : Submodule 𝕜 E<GOAL>U ⟂ Uᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U : Submodule 𝕜 E<GOAL>Uᗮ ⟂ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V : Submodule 𝕜 E<VAR>h : U ⟂ V<GOAL>U ≤ Vᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V : Submodule 𝕜 E<VAR>h : U ⟂ V<GOAL>V ≤ Uᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U : Submodule 𝕜 E<GOAL>U ⟂ ⊤ ↔ U = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>V : Submodule 𝕜 E<GOAL>⊤ ⟂ V ↔ V = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V : Submodule 𝕜 E<VAR>h : U ⟂ V<GOAL>Disjoint U V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U₁ U₂ V : Submodule 𝕜 E<GOAL>U₁ ⊔ U₂ ⟂ V ↔ U₁ ⟂ V ∧ U₂ ⟂ V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U V₁ V₂ : Submodule 𝕜 E<GOAL>U ⟂ V₁ ⊔ V₂ ↔ U ⟂ V₁ ∧ U ⟂ V₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U : Set (Submodule 𝕜 E)<VAR>V : Submodule 𝕜 E<GOAL>sSup U ⟂ V ↔ ∀ Uᵢ ∈ U, Uᵢ ⟂ V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>U : Submodule 𝕜 E<VAR>V : Set (Submodule 𝕜 E)<GOAL>U ⟂ sSup V ↔ ∀ Vᵢ ∈ V, U ⟂ Vᵢ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Sort u_4<VAR>U : ι → Submodule 𝕜 E<VAR>V : Submodule 𝕜 E<GOAL>iSup U ⟂ V ↔ ∀ (i : ι), U i ⟂ V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Sort u_4<VAR>U : Submodule 𝕜 E<VAR>V : ι → Submodule 𝕜 E<GOAL>U ⟂ iSup V ↔ ∀ (i : ι), U ⟂ V i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>s t : Set E<GOAL>Submodule.span 𝕜 s ⟂ Submodule.span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>f : E →ₗᵢ[𝕜] F<VAR>U V : Submodule 𝕜 E<VAR>h : U ⟂ V<GOAL>Submodule.map f U ⟂ Submodule.map f V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>f : E →ₗᵢ[𝕜] F<VAR>U V : Submodule 𝕜 F<VAR>h : U ⟂ V<GOAL>Submodule.comap f U ⟂ Submodule.comap f V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>f : E ≃ₗᵢ[𝕜] F<VAR>U V : Submodule 𝕜 E<GOAL>Submodule.map f U ⟂ Submodule.map f V ↔ U ⟂ V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>f : E ≃ₗᵢ[𝕜] F<VAR>U V : Submodule 𝕜 F<GOAL>Submodule.comap f U ⟂ Submodule.comap f V ↔ U ⟂ V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>V : ι → Submodule 𝕜 E<GOAL>(OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) ↔ Pairwise ((fun x x_1 => x ⟂ x_1) on V)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>V i ⟂ V j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>S : F →ₗ.[𝕜] E<VAR>h : T.IsFormalAdjoint S<GOAL>S.IsFormalAdjoint T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>y : ↥T.adjointDomain<VAR>x : ↥T.domain<GOAL>(T.adjointDomainMkCLM y) x = ⟪↑y, ↑T x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>hT : Dense ↑T.domain<VAR>y : ↥T.adjointDomain<VAR>x : ↥T.domain<GOAL>(LinearPMap.adjointDomainMkCLMExtend hT y) ↑x = ⟪↑y, ↑T x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>hT : Dense ↑T.domain<VAR>CompleteSpace E<VAR>y : ↥T.adjointDomain<VAR>x : ↥T.domain<GOAL>⟪(LinearPMap.adjointAux hT) y, ↑x⟫_𝕜 = ⟪↑y, ↑T x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>hT : Dense ↑T.domain<VAR>CompleteSpace E<VAR>y : ↥T.adjointDomain<VAR>x₀ : E<VAR>hx₀ : ∀ (x : ↥T.domain), ⟪x₀, ↑x⟫_𝕜 = ⟪↑y, ↑T x⟫_𝕜<GOAL>(LinearPMap.adjointAux hT) y = x₀
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>CompleteSpace E<VAR>y : F<GOAL>y ∈ T.adjoint.domain ↔ Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>CompleteSpace E<VAR>y : F<VAR>h : ∃ w, ∀ (x : ↥T.domain), ⟪w, ↑x⟫_𝕜 = ⟪y, ↑T x⟫_𝕜<GOAL>y ∈ T.adjoint.domain
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>CompleteSpace E<VAR>hT : ¬Dense ↑T.domain<VAR>y : ↥T.adjoint.domain<GOAL>↑T.adjoint y = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>hT : Dense ↑T.domain<VAR>CompleteSpace E<VAR>y : ↥T.adjoint.domain<GOAL>↑T.adjoint y = (LinearPMap.adjointAux hT) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>hT : Dense ↑T.domain<VAR>CompleteSpace E<VAR>y : ↥T.adjoint.domain<VAR>x₀ : E<VAR>hx₀ : ∀ (x : ↥T.domain), ⟪x₀, ↑x⟫_𝕜 = ⟪↑y, ↑T x⟫_𝕜<GOAL>↑T.adjoint y = x₀
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>hT : Dense ↑T.domain<VAR>CompleteSpace E<GOAL>T.adjoint.IsFormalAdjoint T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>S : F →ₗ.[𝕜] E<VAR>hT : Dense ↑T.domain<VAR>CompleteSpace E<VAR>h : T.IsFormalAdjoint S<GOAL>S ≤ T.adjoint
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace E<VAR>CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>p : Submodule 𝕜 E<VAR>hp : Dense ↑p<GOAL>((↑A).toPMap p).adjoint = (↑(ContinuousLinearMap.adjoint A)).toPMap ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>A : E →ₗ.[𝕜] E<GOAL>IsSelfAdjoint A ↔ A.adjoint = A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>A : E →ₗ.[𝕜] E<VAR>hA : IsSelfAdjoint A<GOAL>Dense ↑A.domain
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>x : F<GOAL>(MeasureTheory.weightedSMul μ s) x = (μ s).toReal • x
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<GOAL>MeasureTheory.weightedSMul 0 = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.weightedSMul μ ∅ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hνs : ν s ≠ ⊤<GOAL>MeasureTheory.weightedSMul (μ + ν) s = MeasureTheory.weightedSMul μ s + MeasureTheory.weightedSMul ν s
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<VAR>s : Set α<GOAL>MeasureTheory.weightedSMul (c • μ) s = c.toReal • MeasureTheory.weightedSMul μ s
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hst : μ s = μ t<GOAL>MeasureTheory.weightedSMul μ s = MeasureTheory.weightedSMul μ t
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h_zero : μ s = 0<GOAL>MeasureTheory.weightedSMul μ s = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>ht : MeasurableSet t<VAR>hs_finite : μ s ≠ ⊤<VAR>ht_finite : μ t ≠ ⊤<VAR>h_inter : s ∩ t = ∅<GOAL>MeasureTheory.weightedSMul μ (s ∪ t) = MeasureTheory.weightedSMul μ s + MeasureTheory.weightedSMul μ t
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>_hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hs_finite : μ s ≠ ⊤<VAR>ht_finite : μ t ≠ ⊤<VAR>h_inter : s ∩ t = ∅<GOAL>MeasureTheory.weightedSMul μ (s ∪ t) = MeasureTheory.weightedSMul μ s + MeasureTheory.weightedSMul μ t
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>c : 𝕜<VAR>s : Set α<VAR>x : F<GOAL>(MeasureTheory.weightedSMul μ s) (c • x) = c • (MeasureTheory.weightedSMul μ s) x
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>‖MeasureTheory.weightedSMul μ s‖ ≤ (μ s).toReal
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α), MeasureTheory.DominatedFinMeasAdditive μ (MeasureTheory.weightedSMul μ) 1
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>0 ≤ (MeasureTheory.weightedSMul μ s) x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α ℝ<GOAL>MeasureTheory.SimpleFunc.map norm f.posPart = f.posPart
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α ℝ<GOAL>MeasureTheory.SimpleFunc.map norm f.negPart = f.negPart
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α ℝ<GOAL>f.posPart - f.negPart = f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : MeasureTheory.SimpleFunc α F), MeasureTheory.SimpleFunc.integral μ f = MeasureTheory.SimpleFunc.setToSimpleFunc (MeasureTheory.weightedSMul μ) f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α F<GOAL>MeasureTheory.SimpleFunc.integral μ f = ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal • x
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>DecidablePred fun x => x ≠ 0<VAR>m : MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α F<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.SimpleFunc.integral μ f = ∑ x ∈ Finset.filter (fun x => x ≠ 0) f.range, (μ (↑f ⁻¹' {x})).toReal • x
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>DecidablePred fun x => x ≠ 0<VAR>f : MeasureTheory.SimpleFunc α F<VAR>s : Finset F<VAR>hs : Finset.filter (fun x => x ≠ 0) f.range ⊆ s<GOAL>MeasureTheory.SimpleFunc.integral μ f = ∑ x ∈ s, (μ (↑f ⁻¹' {x})).toReal • x
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>y : F<GOAL>MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.const α y) = (μ Set.univ).toReal • y
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α F<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.piecewise s hs f 0) = MeasureTheory.SimpleFunc.integral (μ.restrict s) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>g : E → F<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>hg : g 0 = 0<GOAL>MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map g f) = ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal • g x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>g : E → ℝ≥0∞<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>hg0 : g 0 = 0<VAR>ht : ∀ (b : E), g b ≠ ⊤<GOAL>MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map (ENNReal.toReal ∘ g) f) = (∫⁻ (a : α), g (↑f a) ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>f g : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>h : ↑f =ᵐ[μ] ↑g<GOAL>MeasureTheory.SimpleFunc.integral μ f = MeasureTheory.SimpleFunc.integral μ g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α ℝ<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>h_pos : 0 ≤ᵐ[μ] ↑f<GOAL>MeasureTheory.SimpleFunc.integral μ f = (∫⁻ (a : α), ENNReal.ofReal (↑f a) ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>f g : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>hg : MeasureTheory.Integrable (↑g) μ<GOAL>MeasureTheory.SimpleFunc.integral μ (f + g) = MeasureTheory.SimpleFunc.integral μ f + MeasureTheory.SimpleFunc.integral μ g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>MeasureTheory.SimpleFunc.integral μ (-f) = -MeasureTheory.SimpleFunc.integral μ f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>f g : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>hg : MeasureTheory.Integrable (↑g) μ<GOAL>MeasureTheory.SimpleFunc.integral μ (f - g) = MeasureTheory.SimpleFunc.integral μ f - MeasureTheory.SimpleFunc.integral μ g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>SMulCommClass ℝ 𝕜 E<VAR>c : 𝕜<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>MeasureTheory.SimpleFunc.integral μ (c • f) = c • MeasureTheory.SimpleFunc.integral μ f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>‖MeasureTheory.SimpleFunc.setToSimpleFunc T f‖ ≤ C * MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map norm f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>‖MeasureTheory.SimpleFunc.integral μ f‖ ≤ MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map norm f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>ν : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) (μ + ν)<GOAL>MeasureTheory.SimpleFunc.integral (μ + ν) f = MeasureTheory.SimpleFunc.integral μ f + MeasureTheory.SimpleFunc.integral ν f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>‖f‖ = MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map norm (MeasureTheory.Lp.simpleFunc.toSimpleFunc f))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc ℝ 1 μ)<GOAL>↑(MeasureTheory.L1.SimpleFunc.posPart f) = MeasureTheory.Lp.posPart ↑f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc ℝ 1 μ)<GOAL>↑(MeasureTheory.L1.SimpleFunc.negPart f) = MeasureTheory.Lp.negPart ↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.integral f = MeasureTheory.SimpleFunc.integral μ (MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc ℝ 1 μ)<VAR>h_pos : 0 ≤ᵐ[μ] ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)<GOAL>MeasureTheory.L1.SimpleFunc.integral f = (∫⁻ (a : α), ENNReal.ofReal (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) a) ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.integral f = MeasureTheory.L1.SimpleFunc.setToL1S (MeasureTheory.weightedSMul μ) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>f g : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<VAR>h : ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) =ᵐ[μ] ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc g)<GOAL>MeasureTheory.L1.SimpleFunc.integral f = MeasureTheory.L1.SimpleFunc.integral g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>f g : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.integral (f + g) = MeasureTheory.L1.SimpleFunc.integral f + MeasureTheory.L1.SimpleFunc.integral g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_4<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>SMulCommClass ℝ 𝕜 E<VAR>c : 𝕜<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.integral (c • f) = c • MeasureTheory.L1.SimpleFunc.integral f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>‖MeasureTheory.L1.SimpleFunc.integral f‖ ≤ ‖f‖