ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>l : F → E<VAR>l' : F →L[𝕜] E<VAR>y : F<VAR>hl : HasStrictFDerivAt l l' y<VAR>hf : HasStrictDerivAt f f' x<VAR>hy : y = f x<GOAL>HasStrictDerivAt (l ∘ f) (l' f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>l : F → E<VAR>t : Set F<VAR>hl : DifferentiableWithinAt 𝕜 l t (f x)<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hs : Set.MapsTo f s t<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>l : F → E<VAR>y : F<VAR>t : Set F<VAR>hl : DifferentiableWithinAt 𝕜 l t y<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hs : Set.MapsTo f s t<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hy : y = f x<GOAL>derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>l : F → E<VAR>hl : DifferentiableAt 𝕜 l (f x)<VAR>hf : DifferentiableAt 𝕜 f x<GOAL>deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>x : 𝕜<VAR>l : F → E<VAR>y : F<VAR>hl : DifferentiableAt 𝕜 l y<VAR>hf : DifferentiableAt 𝕜 f x<VAR>hy : y = f x<GOAL>deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>Ring R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower 𝕜 R M<VAR>IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>n : ℕ<GOAL>((NormedSpace.expSeries 𝕜 (tsze R M) n) fun x_1 => x).fst = (NormedSpace.expSeries 𝕜 R n) fun x_1 => x.fst
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>Ring R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower 𝕜 R M<VAR>IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<VAR>n : ℕ<GOAL>((NormedSpace.expSeries 𝕜 (tsze R M) (n + 1)) fun x_1 => x).snd = ((NormedSpace.expSeries 𝕜 R n) fun x_1 => x.fst) • x.snd
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>Ring R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower 𝕜 R M<VAR>IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<VAR>e : R<VAR>h : HasSum (fun n => (NormedSpace.expSeries 𝕜 R n) fun x_1 => x.fst) e<GOAL>HasSum (fun n => ((NormedSpace.expSeries 𝕜 (tsze R M) n) fun x_1 => x).snd) (e • x.snd)
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>Ring R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower 𝕜 R M<VAR>IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<VAR>e : R<VAR>h : HasSum (fun n => (NormedSpace.expSeries 𝕜 R n) fun x_1 => x.fst) e<GOAL>HasSum (fun n => (NormedSpace.expSeries 𝕜 (tsze R M) n) fun x_1 => x) (TrivSqZeroExt.inl e + TrivSqZeroExt.inr (e • x.snd))
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>Ring R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower 𝕜 R M<VAR>IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>T2Space R<VAR>T2Space M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<GOAL>NormedSpace.exp 𝕜 x = TrivSqZeroExt.inl (NormedSpace.exp 𝕜 x.fst) + TrivSqZeroExt.inr (NormedSpace.exp 𝕜 x.fst • x.snd)
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>Ring R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower 𝕜 R M<VAR>IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>T2Space R<VAR>T2Space M<VAR>x : R<GOAL>NormedSpace.exp 𝕜 (TrivSqZeroExt.inl x) = TrivSqZeroExt.inl (NormedSpace.exp 𝕜 x)
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>Ring R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower 𝕜 R M<VAR>IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>T2Space R<VAR>T2Space M<VAR>m : M<GOAL>NormedSpace.exp 𝕜 (TrivSqZeroExt.inr m) = 1 + TrivSqZeroExt.inr m
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>CommRing R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>IsCentralScalar R M<VAR>IsScalarTower 𝕜 R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>T2Space R<VAR>T2Space M<VAR>x : tsze R M<GOAL>NormedSpace.exp 𝕜 x = TrivSqZeroExt.inl (NormedSpace.exp 𝕜 x.fst) + TrivSqZeroExt.inr (NormedSpace.exp 𝕜 x.fst • x.snd)
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>CommRing R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>IsCentralScalar R M<VAR>IsScalarTower 𝕜 R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>T2Space R<VAR>T2Space M<VAR>x : tsze R M<GOAL>(NormedSpace.exp 𝕜 x).fst = NormedSpace.exp 𝕜 x.fst
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>CommRing R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>IsCentralScalar R M<VAR>IsScalarTower 𝕜 R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>T2Space R<VAR>T2Space M<VAR>x : tsze R M<GOAL>(NormedSpace.exp 𝕜 x).snd = NormedSpace.exp 𝕜 x.fst • x.snd
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>CommRing R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>IsCentralScalar R M<VAR>IsScalarTower 𝕜 R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>T2Space R<VAR>T2Space M<VAR>x : tsze R M<VAR>Invertible x.fst<GOAL>x = x.fst • NormedSpace.exp 𝕜 (⅟x.fst • TrivSqZeroExt.inr x.snd)
<VAR>𝕜 : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>Field R<VAR>AddCommGroup M<VAR>Algebra 𝕜 R<VAR>Module 𝕜 M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>IsCentralScalar R M<VAR>IsScalarTower 𝕜 R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>ContinuousSMul R M<VAR>ContinuousSMul Rᵐᵒᵖ M<VAR>T2Space R<VAR>T2Space M<VAR>x : tsze R M<VAR>hx : x.fst ≠ 0<GOAL>x = x.fst • NormedSpace.exp 𝕜 (x.fst⁻¹ • TrivSqZeroExt.inr x.snd)
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>SeminormedRing R<VAR>SeminormedAddCommGroup M<VAR>x : tsze R M<GOAL>‖x‖ = ‖x.fst‖ + ‖x.snd‖
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>SeminormedRing R<VAR>SeminormedAddCommGroup M<VAR>x : tsze R M<GOAL>‖x‖₊ = ‖x.fst‖₊ + ‖x.snd‖₊
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>SeminormedRing R<VAR>SeminormedAddCommGroup M<VAR>r : R<GOAL>‖TrivSqZeroExt.inl r‖ = ‖r‖
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>SeminormedRing R<VAR>SeminormedAddCommGroup M<VAR>m : M<GOAL>‖TrivSqZeroExt.inr m‖ = ‖m‖
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>SeminormedRing R<VAR>SeminormedAddCommGroup M<VAR>r : R<GOAL>‖TrivSqZeroExt.inl r‖₊ = ‖r‖₊
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>SeminormedRing R<VAR>SeminormedAddCommGroup M<VAR>m : M<GOAL>‖TrivSqZeroExt.inr m‖₊ = ‖m‖₊
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>f' : E →L[𝕜'] F<VAR>x : E<VAR>h : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt f (ContinuousLinearMap.restrictScalars 𝕜 f') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>f' : E →L[𝕜'] F<VAR>x : E<VAR>L : Filter E<VAR>h : HasFDerivAtFilter f f' x L<GOAL>HasFDerivAtFilter f (ContinuousLinearMap.restrictScalars 𝕜 f') x L
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>f' : E →L[𝕜'] F<VAR>x : E<VAR>h : HasFDerivAt f f' x<GOAL>HasFDerivAt f (ContinuousLinearMap.restrictScalars 𝕜 f') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>f' : E →L[𝕜'] F<VAR>s : Set E<VAR>x : E<VAR>h : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt f (ContinuousLinearMap.restrictScalars 𝕜 f') s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>x : E<VAR>h : DifferentiableAt 𝕜' f x<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : DifferentiableWithinAt 𝕜' f s x<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>s : Set E<VAR>h : DifferentiableOn 𝕜' f s<GOAL>DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>h : Differentiable 𝕜' f<GOAL>Differentiable 𝕜 f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>f' : E →L[𝕜'] F<VAR>s : Set E<VAR>x : E<VAR>g' : E →L[𝕜] F<VAR>h : HasFDerivWithinAt f g' s x<VAR>H : ContinuousLinearMap.restrictScalars 𝕜 f' = g'<GOAL>HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>f' : E →L[𝕜'] F<VAR>x : E<VAR>g' : E →L[𝕜] F<VAR>h : HasFDerivAt f g' x<VAR>H : ContinuousLinearMap.restrictScalars 𝕜 f' = g'<GOAL>HasFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>x : E<VAR>h : DifferentiableAt 𝕜' f x<GOAL>fderiv 𝕜 f x = ContinuousLinearMap.restrictScalars 𝕜 (fderiv 𝕜' f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hs : UniqueDiffWithinAt 𝕜 s x<GOAL>DifferentiableWithinAt 𝕜' f s x ↔ ∃ g', ContinuousLinearMap.restrictScalars 𝕜 g' = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>x : E<VAR>hf : DifferentiableAt 𝕜 f x<GOAL>DifferentiableAt 𝕜' f x ↔ ∃ g', ContinuousLinearMap.restrictScalars 𝕜 g' = fderiv 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>x : (i : ι) → E i<VAR>i : ι<VAR>y : E i<GOAL>HasFDerivAt (Function.update x i) (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))) y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>i : ι<VAR>y : E i<GOAL>HasFDerivAt (Pi.single i) (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))) y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>x : (i : ι) → E i<VAR>i : ι<VAR>y : E i<GOAL>fderiv 𝕜 (Function.update x i) y = ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type u_3<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>i : ι<VAR>y : E i<GOAL>fderiv 𝕜 (Pi.single i) y = ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : E<GOAL>Monotone fun s => posTangentConeAt s a
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>x y : E<VAR>h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s<GOAL>y ∈ posTangentConeAt s x
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>x y : E<VAR>h : [x-[ℝ]x + y] ⊆ s<GOAL>y ∈ posTangentConeAt s x
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set E<VAR>x y : E<VAR>h : [x-[ℝ]y] ⊆ s<GOAL>y - x ∈ posTangentConeAt s x
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : E<GOAL>posTangentConeAt Set.univ a = Set.univ
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a y : E<VAR>h : IsLocalMaxOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>hy : y ∈ posTangentConeAt s a<GOAL>f' y ≤ 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a y : E<VAR>h : IsLocalMaxOn f s a<VAR>hy : y ∈ posTangentConeAt s a<GOAL>(fderivWithin ℝ f s a) y ≤ 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a y : E<VAR>h : IsLocalMaxOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hy' : -y ∈ posTangentConeAt s a<GOAL>f' y = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a y : E<VAR>h : IsLocalMaxOn f s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hy' : -y ∈ posTangentConeAt s a<GOAL>(fderivWithin ℝ f s a) y = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a y : E<VAR>h : IsLocalMinOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>hy : y ∈ posTangentConeAt s a<GOAL>0 ≤ f' y
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a y : E<VAR>h : IsLocalMinOn f s a<VAR>hy : y ∈ posTangentConeAt s a<GOAL>0 ≤ (fderivWithin ℝ f s a) y
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a y : E<VAR>h : IsLocalMinOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hy' : -y ∈ posTangentConeAt s a<GOAL>f' y = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a y : E<VAR>h : IsLocalMinOn f s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hy' : -y ∈ posTangentConeAt s a<GOAL>(fderivWithin ℝ f s a) y = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>a : E<VAR>h : IsLocalMin f a<VAR>hf : HasFDerivAt f f' a<GOAL>f' = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>a : E<VAR>h : IsLocalMin f a<GOAL>fderiv ℝ f a = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>a : E<VAR>h : IsLocalMax f a<VAR>hf : HasFDerivAt f f' a<GOAL>f' = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>a : E<VAR>h : IsLocalMax f a<GOAL>fderiv ℝ f a = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>a : E<VAR>h : IsLocalExtr f a<GOAL>HasFDerivAt f f' a → f' = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>a : E<VAR>h : IsLocalExtr f a<GOAL>fderiv ℝ f a = 0
<VAR>s : Set ℝ<VAR>a : ℝ<GOAL>1 ∈ posTangentConeAt s a ↔ a ∈ closure (Set.Ioi a ∩ s)
<VAR>s : Set ℝ<VAR>a : ℝ<GOAL>1 ∈ posTangentConeAt s a ↔ ∃ᶠ (x : ℝ) in 𝓝[>] a, x ∈ s
<VAR>f : ℝ → ℝ<VAR>f' a : ℝ<VAR>h : IsLocalMin f a<VAR>hf : HasDerivAt f f' a<GOAL>f' = 0
<VAR>f : ℝ → ℝ<VAR>a : ℝ<VAR>h : IsLocalMin f a<GOAL>deriv f a = 0
<VAR>f : ℝ → ℝ<VAR>f' a : ℝ<VAR>h : IsLocalMax f a<VAR>hf : HasDerivAt f f' a<GOAL>f' = 0
<VAR>f : ℝ → ℝ<VAR>a : ℝ<VAR>h : IsLocalMax f a<GOAL>deriv f a = 0
<VAR>f : ℝ → ℝ<VAR>f' a : ℝ<VAR>h : IsLocalExtr f a<GOAL>HasDerivAt f f' a → f' = 0
<VAR>f : ℝ → ℝ<VAR>a : ℝ<VAR>h : IsLocalExtr f a<GOAL>deriv f a = 0
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>A : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → MeasureTheory.Measure (A i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq ι<VAR>p : ℝ<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>x : (i : ι) → A i<GOAL>MeasureTheory.GridLines.T μ p f Finset.univ x = ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (t : A i), f (Function.update x i t) ∂μ i) ^ p ∂MeasureTheory.Measure.pi μ
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → MeasureTheory.Measure (A i)<VAR>DecidableEq ι<VAR>p : ℝ<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>x : (i : ι) → A i<GOAL>MeasureTheory.GridLines.T μ p f ∅ x = f x ^ (1 + p)
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → MeasureTheory.Measure (A i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>s : Finset ι<VAR>hp : ↑s.card * p ≤ 1<VAR>i : ι<VAR>hi : i ∉ s<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<GOAL>MeasureTheory.GridLines.T μ p f (insert i s) ≤ MeasureTheory.GridLines.T μ p (∫⋯∫⁻_{i}, f ∂μ) s
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>A : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → MeasureTheory.Measure (A i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Antitone fun s => MeasureTheory.GridLines.T μ p (∫⋯∫⁻_sᶜ, f ∂μ) s
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>A : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → MeasureTheory.Measure (A i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (Function.update x i xᵢ) ∂μ i) ^ p ∂MeasureTheory.Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂MeasureTheory.Measure.pi μ) ^ (1 + p)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>A : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → MeasureTheory.Measure (A i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite (μ i)<VAR>DecidableEq ι<VAR>p : ℝ<VAR>hp : (↑#ι).IsConjExponent p<VAR>f : ((a : ι) → A a) → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (x : (i : ι) → A i), ∏ i : ι, (∫⁻ (xᵢ : A i), f (Function.update x i xᵢ) ∂μ i) ^ (1 / (↑#ι - 1)) ∂MeasureTheory.Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂MeasureTheory.Measure.pi μ) ^ p
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>p : ℝ<VAR>hp : (↑#ι).IsConjExponent p<VAR>u : (ι → ℝ) → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<GOAL>∫⁻ (x : ι → ℝ), ↑‖u x‖₊ ^ p ≤ (∫⁻ (x : ι → ℝ), ↑‖fderiv ℝ u x‖₊) ^ p
<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>p : ℝ<GOAL>MeasureTheory.lintegralPowLePowLIntegralFDerivConst μ p = let ι := Fin (FiniteDimensional.finrank ℝ E); let_fun this := ⋯; let e := ContinuousLinearEquiv.ofFinrankEq this; let c := μ.addHaarScalarFactor (MeasureTheory.Measure.map (⇑e.symm) MeasureTheory.volume); c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹