ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>c : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f = c • (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hC : 0 ≤ C<GOAL>‖MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT‖ ≤ C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<GOAL>‖MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT‖ ≤ max C 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>x : E<GOAL>(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) (MeasureTheory.Lp.simpleFunc.indicatorConst 1 ⋯ ⋯ x) = (T Set.univ) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>T T' : Set α → E →L[ℝ] G''<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>T T' : Set α → E →L[ℝ] G''<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>NormedLatticeAddCommGroup G'<VAR>NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : ↥(MeasureTheory.Lp.simpleFunc G' 1 μ)<VAR>hf : 0 ≤ f<GOAL>0 ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α G' μ hT) f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>NormedLatticeAddCommGroup G'<VAR>NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : ↥(MeasureTheory.Lp.simpleFunc G' 1 μ)<VAR>hfg : f ≤ g<GOAL>(MeasureTheory.L1.SimpleFunc.setToL1SCLM α G' μ hT) f ≤ (MeasureTheory.L1.SimpleFunc.setToL1SCLM α G' μ hT) g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 hT) ↑f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 hT) f = (MeasureTheory.L1.setToL1' 𝕜 hT h_smul) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ 0 C<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 hT) f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 hT) f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>h : T = T'<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 hT) f = (MeasureTheory.L1.setToL1 hT') f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 hT) f = (MeasureTheory.L1.setToL1 hT') f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 ⋯) f = (MeasureTheory.L1.setToL1 hT) f + (MeasureTheory.L1.setToL1 hT') f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>hT'' : MeasureTheory.DominatedFinMeasAdditive μ T'' C''<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 hT'') f = (MeasureTheory.L1.setToL1 hT) f + (MeasureTheory.L1.setToL1 hT') f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>c : ℝ<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 ⋯) f = c • (MeasureTheory.L1.setToL1 hT) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 hT') f = c • (MeasureTheory.L1.setToL1 hT) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x<VAR>c : 𝕜<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 hT) (c • f) = c • (MeasureTheory.L1.setToL1 hT) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>x : E<GOAL>(MeasureTheory.L1.setToL1 hT) ↑(MeasureTheory.Lp.simpleFunc.indicatorConst 1 hs ⋯ x) = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<GOAL>(MeasureTheory.L1.setToL1 hT) (MeasureTheory.indicatorConstLp 1 hs hμs x) = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>x : E<GOAL>(MeasureTheory.L1.setToL1 hT) (MeasureTheory.indicatorConstLp 1 ⋯ ⋯ x) = (T Set.univ) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>CompleteSpace G''<VAR>T T' : Set α → E →L[ℝ] G''<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 hT) f ≤ (MeasureTheory.L1.setToL1 hT') f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>CompleteSpace G''<VAR>T T' : Set α → E →L[ℝ] G''<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>(MeasureTheory.L1.setToL1 hT) f ≤ (MeasureTheory.L1.setToL1 hT') f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>CompleteSpace G''<VAR>NormedLatticeAddCommGroup G'<VAR>NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : ↥(MeasureTheory.Lp G' 1 μ)<VAR>hf : 0 ≤ f<GOAL>0 ≤ (MeasureTheory.L1.setToL1 hT) f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>CompleteSpace G''<VAR>NormedLatticeAddCommGroup G'<VAR>NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : ↥(MeasureTheory.Lp G' 1 μ)<VAR>hfg : f ≤ g<GOAL>(MeasureTheory.L1.setToL1 hT) f ≤ (MeasureTheory.L1.setToL1 hT) g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<GOAL>‖MeasureTheory.L1.setToL1 hT‖ ≤ ‖MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hC : 0 ≤ C<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>‖(MeasureTheory.L1.setToL1 hT) f‖ ≤ C * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>‖(MeasureTheory.L1.setToL1 hT) f‖ ≤ max C 0 * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hC : 0 ≤ C<GOAL>‖MeasureTheory.L1.setToL1 hT‖ ≤ C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<GOAL>‖MeasureTheory.L1.setToL1 hT‖ ≤ max C 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<GOAL>LipschitzWith C.toNNReal ⇑(MeasureTheory.L1.setToL1 hT)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<VAR>ι : Type u_7<VAR>fs : ι → ↥(MeasureTheory.Lp E 1 μ)<VAR>l : Filter ι<VAR>hfs : Filter.Tendsto fs l (𝓝 f)<GOAL>Filter.Tendsto (fun i => (MeasureTheory.L1.setToL1 hT) (fs i)) l (𝓝 ((MeasureTheory.L1.setToL1 hT) f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.setToFun μ T hT f = (MeasureTheory.L1.setToL1 hT) (MeasureTheory.Integrable.toL1 f hf)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>MeasureTheory.setToFun μ T hT ↑↑f = (MeasureTheory.L1.setToL1 hT) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hf : ¬MeasureTheory.Integrable f μ<GOAL>MeasureTheory.setToFun μ T hT f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hf : ¬MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.setToFun μ T hT f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>h : T = T'<VAR>f : α → E<GOAL>MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ T' hT' f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s<VAR>f : α → E<GOAL>MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ T' hT' f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>f : α → E<GOAL>MeasureTheory.setToFun μ (T + T') ⋯ f = MeasureTheory.setToFun μ T hT f + MeasureTheory.setToFun μ T' hT' f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>hT'' : MeasureTheory.DominatedFinMeasAdditive μ T'' C''<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : α → E<GOAL>MeasureTheory.setToFun μ T'' hT'' f = MeasureTheory.setToFun μ T hT f + MeasureTheory.setToFun μ T' hT' f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>c : ℝ<VAR>f : α → E<GOAL>MeasureTheory.setToFun μ (fun s => c • T s) ⋯ f = c • MeasureTheory.setToFun μ T hT f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T T' : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : α → E<GOAL>MeasureTheory.setToFun μ T' hT' f = c • MeasureTheory.setToFun μ T hT f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<GOAL>MeasureTheory.setToFun μ T hT 0 = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>C : ℝ<VAR>f : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ 0 C<GOAL>MeasureTheory.setToFun μ 0 hT f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0<GOAL>MeasureTheory.setToFun μ T hT f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f g : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.setToFun μ T hT (f + g) = MeasureTheory.setToFun μ T hT f + MeasureTheory.setToFun μ T hT g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → α → E<VAR>hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ<GOAL>MeasureTheory.setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, MeasureTheory.setToFun μ T hT (f i)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → α → E<VAR>hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ<GOAL>(MeasureTheory.setToFun μ T hT fun a => ∑ i ∈ s, f i a) = ∑ i ∈ s, MeasureTheory.setToFun μ T hT (f i)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>f : α → E<GOAL>MeasureTheory.setToFun μ T hT (-f) = -MeasureTheory.setToFun μ T hT f