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' T'' : Set α → E →L[ℝ] F<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T'' f = MeasureTheory.SimpleFunc.setToSimpleFunc T f + MeasureTheory.SimpleFunc.setToSimpleFunc T' f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>T : Set α → F →L[ℝ] F'<VAR>c : ℝ<VAR>f : MeasureTheory.SimpleFunc α F<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc (fun s => c • T s) f = c • MeasureTheory.SimpleFunc.setToSimpleFunc T f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F' : Type u_4<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 : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T' f = c • MeasureTheory.SimpleFunc.setToSimpleFunc T 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>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>f g : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>hg : MeasureTheory.Integrable (↑g) μ<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T (f + g) = MeasureTheory.SimpleFunc.setToSimpleFunc T f + MeasureTheory.SimpleFunc.setToSimpleFunc T 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>T : Set α → E →L[ℝ] F<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T (-f) = -MeasureTheory.SimpleFunc.setToSimpleFunc T 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>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>f g : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>hg : MeasureTheory.Integrable (↑g) μ<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T (f - g) = MeasureTheory.SimpleFunc.setToSimpleFunc T f - MeasureTheory.SimpleFunc.setToSimpleFunc T 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>T : Set α → E →L[ℝ] F<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>c : ℝ<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T (c • f) = c • MeasureTheory.SimpleFunc.setToSimpleFunc T f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_6<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>NormedSpace 𝕜 F<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x<VAR>c : 𝕜<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T (c • f) = c • MeasureTheory.SimpleFunc.setToSimpleFunc T f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>m : MeasurableSpace α<VAR>T T' : Set α → F →L[ℝ] G''<VAR>hTT' : ∀ (s : Set α) (x : F), (T s) x ≤ (T' s) x<VAR>f : MeasureTheory.SimpleFunc α F<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T f ≤ MeasureTheory.SimpleFunc.setToSimpleFunc T' 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>hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T f ≤ MeasureTheory.SimpleFunc.setToSimpleFunc T' f
<VAR>α : Type u_1<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>NormedLatticeAddCommGroup G'<VAR>NormedSpace ℝ G'<VAR>m : MeasurableSpace α<VAR>T : Set α → G' →L[ℝ] G''<VAR>hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : MeasureTheory.SimpleFunc α G'<VAR>hf : 0 ≤ f<GOAL>0 ≤ MeasureTheory.SimpleFunc.setToSimpleFunc T 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>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : MeasureTheory.SimpleFunc α G'<VAR>hf : 0 ≤ f<VAR>hfi : MeasureTheory.Integrable (↑f) μ<GOAL>0 ≤ MeasureTheory.SimpleFunc.setToSimpleFunc T 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>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : MeasureTheory.SimpleFunc α G'<VAR>hfi : MeasureTheory.Integrable (↑f) μ<VAR>hgi : MeasureTheory.Integrable (↑g) μ<VAR>hfg : f ≤ g<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T f ≤ MeasureTheory.SimpleFunc.setToSimpleFunc T g
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>T : Set α → F' →L[ℝ] F<VAR>f : MeasureTheory.SimpleFunc α F'<GOAL>‖MeasureTheory.SimpleFunc.setToSimpleFunc T f‖ ≤ ∑ x ∈ f.range, ‖T (↑f ⁻¹' {x})‖ * ‖x‖
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : MeasureTheory.SimpleFunc α F<GOAL>‖MeasureTheory.SimpleFunc.setToSimpleFunc T f‖ ≤ C * ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal * ‖x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F' : Type u_4<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_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 * ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal * ‖x‖
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : F<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α x) (MeasureTheory.SimpleFunc.const α 0)) = (T s) x
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>Nonempty α<VAR>T : Set α → F →L[ℝ] F'<VAR>x : F<VAR>m : MeasurableSpace α<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.const α x) = (T Set.univ) x
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>x : F<VAR>m : MeasurableSpace α<GOAL>MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.const α x) = (T Set.univ) x
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc G 1 μ)<GOAL>‖f‖ = ∑ x ∈ (MeasureTheory.Lp.simpleFunc.toSimpleFunc f).range, (μ (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) ⁻¹' {x})).toReal * ‖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>T : Set α → E →L[ℝ] F<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T f = MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.Lp.simpleFunc.toSimpleFunc 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>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S 0 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>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T 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>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>f g : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<VAR>h : ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) =ᵐ[μ] ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc g)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T f = MeasureTheory.L1.SimpleFunc.setToL1S T 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>T T' : Set α → E →L[ℝ] F<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T f = MeasureTheory.L1.SimpleFunc.setToL1S T' 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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>hμ : μ ≪ μ'<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<VAR>f' : ↥(MeasureTheory.Lp.simpleFunc E 1 μ')<VAR>h : ↑↑↑f =ᵐ[μ] ↑↑↑f'<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T f = MeasureTheory.L1.SimpleFunc.setToL1S T 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 T' : Set α → E →L[ℝ] F<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S (T + T') f = MeasureTheory.L1.SimpleFunc.setToL1S T f + MeasureTheory.L1.SimpleFunc.setToL1S T' 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 T' T'' : Set α → E →L[ℝ] F<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T'' f = MeasureTheory.L1.SimpleFunc.setToL1S T f + MeasureTheory.L1.SimpleFunc.setToL1S T' 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>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S (fun s => c • T s) f = c • MeasureTheory.L1.SimpleFunc.setToL1S T 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 T' : Set α → E →L[ℝ] F<VAR>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.setToL1S T' f = c • MeasureTheory.L1.SimpleFunc.setToL1S T 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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>f g : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T (f + g) = MeasureTheory.L1.SimpleFunc.setToL1S T f + MeasureTheory.L1.SimpleFunc.setToL1S T 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>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T (-f) = -MeasureTheory.L1.SimpleFunc.setToL1S T 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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>f g : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T (f - g) = MeasureTheory.L1.SimpleFunc.setToL1S T f - MeasureTheory.L1.SimpleFunc.setToL1S T 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>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>c : ℝ<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T (c • f) = c • MeasureTheory.L1.SimpleFunc.setToL1S T f
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>𝕜 : Type u_6<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedField 𝕜<VAR>E : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x<VAR>c : 𝕜<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T (c • f) = c • MeasureTheory.L1.SimpleFunc.setToL1S T 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_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>‖MeasureTheory.L1.SimpleFunc.setToL1S T 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>T : Set α → E →L[ℝ] F<VAR>s : Set α<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>x : E<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T (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>MeasureTheory.IsFiniteMeasure μ<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<VAR>x : E<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T (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_7<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>T T' : Set α → E →L[ℝ] G''<VAR>hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.L1.SimpleFunc.setToL1S T f ≤ MeasureTheory.L1.SimpleFunc.setToL1S T' 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_7<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>T T' : Set α → E →L[ℝ] G''<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.setToL1S T f ≤ MeasureTheory.L1.SimpleFunc.setToL1S T' 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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<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.setToL1S T 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>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : MeasureTheory.FinMeasAdditive μ T<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.setToL1S T f ≤ MeasureTheory.L1.SimpleFunc.setToL1S T 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>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ 0 C<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ 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>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.simpleFunc E 1 μ)<GOAL>(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ 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>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.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>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>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.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>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 C' : ℝ<VAR>μ' : MeasureTheory.Measure α<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ' T C'<VAR>hμ : μ ≪ μ'<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<VAR>f' : ↥(MeasureTheory.Lp.simpleFunc E 1 μ')<VAR>h : ↑↑↑f =ᵐ[μ] ↑↑↑f'<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>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>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ ⋯) f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f + (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 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.simpleFunc E 1 μ)<GOAL>(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT'') f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f + (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>c : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>(MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ ⋯) f = c • (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f