ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z : ℂ<VAR>hd : DifferentiableOn ℂ f (Metric.ball c R₁)<VAR>h_maps : Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂)<VAR>hz : z ∈ Metric.ball c R₁<GOAL>‖dslope f c z‖ ≤ R₂ / R₁
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z₀ : ℂ<VAR>CompleteSpace E<VAR>StrictConvexSpace ℝ E<VAR>hd : DifferentiableOn ℂ f (Metric.ball c R₁)<VAR>h_maps : Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂)<VAR>h_z₀ : z₀ ∈ Metric.ball c R₁<VAR>h_eq : ‖dslope f c z₀‖ = R₂ / R₁<GOAL>Set.EqOn f (fun z => f c + (z - c) • dslope f c z₀) (Metric.ball c R₁)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c : ℂ<VAR>CompleteSpace E<VAR>StrictConvexSpace ℝ E<VAR>hd : DifferentiableOn ℂ f (Metric.ball c R₁)<VAR>h_maps : Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂)<VAR>h_z₀ : ∃ z₀ ∈ Metric.ball c R₁, ‖dslope f c z₀‖ = R₂ / R₁<GOAL>∃ C, ‖C‖ = R₂ / R₁ ∧ Set.EqOn f (fun z => f c + (z - c) • C) (Metric.ball c R₁)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : DifferentiableOn ℂ f (Metric.ball c R₁)<VAR>h_maps : Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂)<VAR>h₀ : 0 < R₁<GOAL>‖deriv f c‖ ≤ R₂ / R₁
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z : ℂ<VAR>hd : DifferentiableOn ℂ f (Metric.ball c R₁)<VAR>h_maps : Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂)<VAR>hz : z ∈ Metric.ball c R₁<GOAL>dist (f z) (f c) ≤ R₂ / R₁ * dist z c
<VAR>f : ℂ → ℂ<VAR>c : ℂ<VAR>R₁ R₂ : ℝ<VAR>hd : DifferentiableOn ℂ f (Metric.ball c R₁)<VAR>h_maps : Set.MapsTo f (Metric.ball c R₁) (Metric.ball (f c) R₂)<VAR>h₀ : 0 < R₁<GOAL>Complex.abs (deriv f c) ≤ R₂ / R₁
<VAR>f : ℂ → ℂ<VAR>c : ℂ<VAR>R : ℝ<VAR>hd : DifferentiableOn ℂ f (Metric.ball c R)<VAR>h_maps : Set.MapsTo f (Metric.ball c R) (Metric.ball c R)<VAR>hc : f c = c<VAR>h₀ : 0 < R<GOAL>Complex.abs (deriv f c) ≤ 1
<VAR>f : ℂ → ℂ<VAR>c z : ℂ<VAR>R : ℝ<VAR>hd : DifferentiableOn ℂ f (Metric.ball c R)<VAR>h_maps : Set.MapsTo f (Metric.ball c R) (Metric.ball c R)<VAR>hc : f c = c<VAR>hz : z ∈ Metric.ball c R<GOAL>dist (f z) c ≤ dist z c
<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>R : ℝ<VAR>hd : DifferentiableOn ℂ f (Metric.ball 0 R)<VAR>h_maps : Set.MapsTo f (Metric.ball 0 R) (Metric.ball 0 R)<VAR>h₀ : f 0 = 0<VAR>hz : Complex.abs z < R<GOAL>Complex.abs (f z) ≤ Complex.abs z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>U : Set ℂ<VAR>z : ℂ<VAR>r : ℝ<VAR>f : ℂ → E<VAR>hU : IsOpen U<VAR>hf : DifferentiableOn ℂ f U<VAR>hr : 0 < r<VAR>hzr : Metric.closedBall z r ⊆ U<GOAL>Complex.cderiv r f z = deriv f z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>z : ℂ<VAR>M r : ℝ<VAR>f : ℂ → E<VAR>hr : 0 < r<VAR>hf : ∀ w ∈ Metric.sphere z r, ‖f w‖ ≤ M<GOAL>‖Complex.cderiv r f z‖ ≤ M / r
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>z : ℂ<VAR>r : ℝ<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ContinuousOn f (Metric.sphere z r)<VAR>hg : ContinuousOn g (Metric.sphere z r)<GOAL>Complex.cderiv r (f - g) z = Complex.cderiv r f z - Complex.cderiv r g z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>z : ℂ<VAR>M r : ℝ<VAR>f : ℂ → E<VAR>hr : 0 < r<VAR>hfM : ∀ w ∈ Metric.sphere z r, ‖f w‖ < M<VAR>hf : ContinuousOn f (Metric.sphere z r)<GOAL>‖Complex.cderiv r f z‖ < M / r
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>z : ℂ<VAR>M r : ℝ<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hfg : ∀ w ∈ Metric.sphere z r, ‖f w - g w‖ < M<VAR>hf : ContinuousOn f (Metric.sphere z r)<VAR>hg : ContinuousOn g (Metric.sphere z r)<GOAL>‖Complex.cderiv r f z - Complex.cderiv r g z‖ < M / r
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>K : Set ℂ<VAR>δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f : ℂ → E<VAR>hF : TendstoUniformlyOn F f φ (Metric.cthickening δ K)<VAR>hδ : 0 < δ<VAR>hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (Metric.cthickening δ K)<GOAL>TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>U K : Set ℂ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f : ℂ → E<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : Metric.cthickening δ K ⊆ U<GOAL>TendstoUniformlyOn (deriv ∘ F) (Complex.cderiv δ f) φ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>U K : Set ℂ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f : ℂ → E<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ δ > 0, Metric.cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (Complex.cderiv δ f) φ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>U : Set ℂ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f : ℂ → E<VAR>φ.NeBot<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>hU : IsOpen U<GOAL>DifferentiableOn ℂ f U
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>U : Set ℂ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f : ℂ → E<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>hU : IsOpen U<GOAL>TendstoLocallyUniformlyOn (deriv ∘ F) (deriv f) φ U
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>U : Set ℂ<VAR>F : ι → ℂ → E<VAR>u : ι → ℝ<VAR>hu : Summable u<VAR>hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U<VAR>hU : IsOpen U<VAR>hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i<GOAL>DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>U : Set ℂ<VAR>z : ℂ<VAR>F : ι → ℂ → E<VAR>u : ι → ℝ<VAR>hu : Summable u<VAR>hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U<VAR>hU : IsOpen U<VAR>hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i<VAR>hz : z ∈ U<GOAL>HasSum (fun i => deriv (F i) z) (deriv (fun w => ∑' (i : ι), F i w) z)
<VAR>ι : Type u_3<VAR>p : Filter ι<VAR>f : ι → ℂ → ℂ<VAR>g : ℂ → ℂ<VAR>s : Set ℂ<VAR>hs : IsOpen s<VAR>x : ↑s<VAR>hF : TendstoLocallyUniformlyOn f g p s<VAR>hf : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (f n) s<VAR>hg : g ↑x ≠ 0<GOAL>Filter.Tendsto (fun n => logDeriv (f n) ↑x) p (𝓝 (logDeriv g ↑x))
<GOAL>IsConformalMap ↑{ toLinearEquiv := Complex.conjLIE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace ℂ E<VAR>map : ℂ →L[ℂ] E<VAR>nonzero : map ≠ 0<GOAL>IsConformalMap (ContinuousLinearMap.restrictScalars ℝ map)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace ℂ E<VAR>map : ℂ →L[ℂ] E<VAR>nonzero : map ≠ 0<GOAL>IsConformalMap ((ContinuousLinearMap.restrictScalars ℝ map).comp ↑Complex.conjCLE)
<VAR>g : ℂ →L[ℝ] ℂ<VAR>h : IsConformalMap g<GOAL>(∃ map, ContinuousLinearMap.restrictScalars ℝ map = g) ∨ ∃ map, ContinuousLinearMap.restrictScalars ℝ map = g.comp ↑Complex.conjCLE
<VAR>g : ℂ →L[ℝ] ℂ<GOAL>IsConformalMap g ↔ ((∃ map, ContinuousLinearMap.restrictScalars ℝ map = g) ∨ ∃ map, ContinuousLinearMap.restrictScalars ℝ map = g.comp ↑Complex.conjCLE) ∧ g ≠ 0
<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ContinuousOn B (Set.Icc a b)<VAR>hB' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x<VAR>bound : ∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → f x ≤ B x
<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ∀ (x : ℝ), HasDerivAt B (B' x) x<VAR>bound : ∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → f x ≤ B x
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ContinuousOn B (Set.Icc a b)<VAR>hB' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x<VAR>bound : ∀ x ∈ Set.Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → f x ≤ B x
<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ContinuousOn B (Set.Icc a b)<VAR>hB' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x<VAR>bound : ∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → f x ≤ B x
<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ∀ (x : ℝ), HasDerivAt B (B' x) x<VAR>bound : ∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → f x ≤ B x
<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ContinuousOn B (Set.Icc a b)<VAR>hB' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x<VAR>bound : ∀ x ∈ Set.Ico a b, f' x ≤ B' x<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → f x ≤ B x
<VAR>a b : ℝ<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>f' : ℝ → ℝ<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope (norm ∘ f) x z < r<VAR>B B' : ℝ → ℝ<VAR>ha : ‖f a‖ ≤ B a<VAR>hB : ContinuousOn B (Set.Icc a b)<VAR>hB' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x<VAR>bound : ∀ x ∈ Set.Ico a b, ‖f x‖ = B x → f' x < B' x<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → ‖f x‖ ≤ B x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x<VAR>B B' : ℝ → ℝ<VAR>ha : ‖f a‖ ≤ B a<VAR>hB : ContinuousOn B (Set.Icc a b)<VAR>hB' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x<VAR>bound : ∀ x ∈ Set.Ico a b, ‖f x‖ = B x → ‖f' x‖ < B' x<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → ‖f x‖ ≤ B x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x<VAR>B B' : ℝ → ℝ<VAR>ha : ‖f a‖ ≤ B a<VAR>hB : ∀ (x : ℝ), HasDerivAt B (B' x) x<VAR>bound : ∀ x ∈ Set.Ico a b, ‖f x‖ = B x → ‖f' x‖ < B' x<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → ‖f x‖ ≤ B x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x<VAR>B B' : ℝ → ℝ<VAR>ha : ‖f a‖ ≤ B a<VAR>hB : ContinuousOn B (Set.Icc a b)<VAR>hB' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x<VAR>bound : ∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ B' x<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → ‖f x‖ ≤ B x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x<VAR>B B' : ℝ → ℝ<VAR>ha : ‖f a‖ ≤ B a<VAR>hB : ∀ (x : ℝ), HasDerivAt B (B' x) x<VAR>bound : ∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ B' x<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → ‖f x‖ ≤ B x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>C : ℝ<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x<VAR>bound : ∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ C<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → ‖f x - f a‖ ≤ C * (x - a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>C : ℝ<VAR>hf : ∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x<VAR>bound : ∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ C<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → ‖f x - f a‖ ≤ C * (x - a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b C : ℝ<VAR>hf : DifferentiableOn ℝ f (Set.Icc a b)<VAR>bound : ∀ x ∈ Set.Ico a b, ‖derivWithin f (Set.Icc a b) x‖ ≤ C<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → ‖f x - f a‖ ≤ C * (x - a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f f' : ℝ → E<VAR>C : ℝ<VAR>hf : ∀ x ∈ Set.Icc 0 1, HasDerivWithinAt f (f' x) (Set.Icc 0 1) x<VAR>bound : ∀ x ∈ Set.Ico 0 1, ‖f' x‖ ≤ C<GOAL>‖f 1 - f 0‖ ≤ C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>C : ℝ<VAR>hf : DifferentiableOn ℝ f (Set.Icc 0 1)<VAR>bound : ∀ x ∈ Set.Ico 0 1, ‖derivWithin f (Set.Icc 0 1) x‖ ≤ C<GOAL>‖f 1 - f 0‖ ≤ C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hcont : ContinuousOn f (Set.Icc a b)<VAR>hderiv : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f 0 (Set.Ici x) x<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → f x = f a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hdiff : DifferentiableOn ℝ f (Set.Icc a b)<VAR>hderiv : ∀ x ∈ Set.Ico a b, derivWithin f (Set.Icc a b) x = 0<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → f x = f a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' g : ℝ → E<VAR>derivf : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x<VAR>derivg : ∀ x ∈ Set.Ico a b, HasDerivWithinAt g (f' x) (Set.Ici x) x<VAR>fcont : ContinuousOn f (Set.Icc a b)<VAR>gcont : ContinuousOn g (Set.Icc a b)<VAR>hi : f a = g a<VAR>y : ℝ<GOAL>y ∈ Set.Icc a b → f y = g y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>g : ℝ → E<VAR>fdiff : DifferentiableOn ℝ f (Set.Icc a b)<VAR>gdiff : DifferentiableOn ℝ g (Set.Icc a b)<VAR>hderiv : Set.EqOn (derivWithin f (Set.Icc a b)) (derivWithin g (Set.Icc a b)) (Set.Ico a b)<VAR>hi : f a = g a<VAR>y : ℝ<GOAL>y ∈ Set.Icc a b → f y = g y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' : E → E →L[𝕜] G<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<GOAL>‖f y - f x‖ ≤ C * ‖y - x‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → G<VAR>s : Set E<VAR>f' : E → E →L[𝕜] G<VAR>C : ℝ≥0<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C<VAR>hs : Convex ℝ s<GOAL>LipschitzOnWith C f s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>x : E<VAR>f' : E → E →L[𝕜] G<VAR>hs : Convex ℝ s<VAR>f : E → G<VAR>hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y<VAR>hcont : ContinuousWithinAt f' s x<VAR>K : ℝ≥0<VAR>hK : ‖f' x‖₊ < K<GOAL>∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>x : E<VAR>f' : E → E →L[𝕜] G<VAR>hs : Convex ℝ s<VAR>f : E → G<VAR>hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y<VAR>hcont : ContinuousWithinAt f' s x<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>hf : DifferentiableOn 𝕜 f s<VAR>bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<GOAL>‖f y - f x‖ ≤ C * ‖y - x‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → G<VAR>s : Set E<VAR>C : ℝ≥0<VAR>hf : DifferentiableOn 𝕜 f s<VAR>bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖₊ ≤ C<VAR>hs : Convex ℝ s<GOAL>LipschitzOnWith C f s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x<VAR>bound : ∀ x ∈ s, ‖fderiv 𝕜 f x‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<GOAL>‖f y - f x‖ ≤ C * ‖y - x‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → G<VAR>s : Set E<VAR>C : ℝ≥0<VAR>hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x<VAR>bound : ∀ x ∈ s, ‖fderiv 𝕜 f x‖₊ ≤ C<VAR>hs : Convex ℝ s<GOAL>LipschitzOnWith C f s
<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : E → G<VAR>C : ℝ≥0<VAR>hf : Differentiable 𝕜 f<VAR>bound : ∀ (x : E), ‖fderiv 𝕜 f x‖₊ ≤ C<GOAL>LipschitzWith C f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<GOAL>‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>φ : E →L[𝕜] G<VAR>hf : DifferentiableOn 𝕜 f s<VAR>bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x - φ‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<GOAL>‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>φ : E →L[𝕜] G<VAR>hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x<VAR>bound : ∀ x ∈ s, ‖fderiv 𝕜 f x - φ‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<GOAL>‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → G<VAR>s : Set E<VAR>x y : E<VAR>hs : Convex ℝ s<VAR>hf : DifferentiableOn 𝕜 f s<VAR>hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = 0<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f x = f y
<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : E → G<VAR>hf : Differentiable 𝕜 f<VAR>hf' : ∀ (x : E), fderiv 𝕜 f x = 0<VAR>x y : E<GOAL>f x = f y
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f g : E → G<VAR>s : Set E<VAR>x : E<VAR>hs : Convex ℝ s<VAR>hf : DifferentiableOn 𝕜 f s<VAR>hg : DifferentiableOn 𝕜 g s<VAR>hs' : UniqueDiffOn 𝕜 s<VAR>hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x<VAR>hx : x ∈ s<VAR>hfgx : f x = g x<GOAL>Set.EqOn f g s
<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : E → G<VAR>hf : Differentiable 𝕜 f<VAR>hg : Differentiable 𝕜 g<VAR>hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x<VAR>x : E<VAR>hfgx : f x = g x<GOAL>f = g
<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f f' : 𝕜 → G<VAR>s : Set 𝕜<VAR>x y : 𝕜<VAR>C : ℝ<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<GOAL>‖f y - f x‖ ≤ C * ‖y - x‖
<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f f' : 𝕜 → G<VAR>s : Set 𝕜<VAR>C : ℝ≥0<VAR>hs : Convex ℝ s<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C<GOAL>LipschitzOnWith C f s
<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : 𝕜 → G<VAR>s : Set 𝕜<VAR>x y : 𝕜<VAR>C : ℝ<VAR>hf : DifferentiableOn 𝕜 f s<VAR>bound : ∀ x ∈ s, ‖derivWithin f s x‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<GOAL>‖f y - f x‖ ≤ C * ‖y - x‖
<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : 𝕜 → G<VAR>s : Set 𝕜<VAR>C : ℝ≥0<VAR>hs : Convex ℝ s<VAR>hf : DifferentiableOn 𝕜 f s<VAR>bound : ∀ x ∈ s, ‖derivWithin f s x‖₊ ≤ C<GOAL>LipschitzOnWith C f s
<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : 𝕜 → G<VAR>s : Set 𝕜<VAR>x y : 𝕜<VAR>C : ℝ<VAR>hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x<VAR>bound : ∀ x ∈ s, ‖deriv f x‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<GOAL>‖f y - f x‖ ≤ C * ‖y - x‖
<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : 𝕜 → G<VAR>s : Set 𝕜<VAR>C : ℝ≥0<VAR>hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x<VAR>bound : ∀ x ∈ s, ‖deriv f x‖₊ ≤ C<VAR>hs : Convex ℝ s<GOAL>LipschitzOnWith C f s
<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : 𝕜 → G<VAR>C : ℝ≥0<VAR>hf : Differentiable 𝕜 f<VAR>bound : ∀ (x : 𝕜), ‖deriv f x‖₊ ≤ C<GOAL>LipschitzWith C f
<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>RCLike 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : 𝕜 → G<VAR>hf : Differentiable 𝕜 f<VAR>hf' : ∀ (x : 𝕜), deriv f x = 0<VAR>x y : 𝕜<GOAL>f x = f y
<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Set.Icc a b)<VAR>hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Set.Icc a b)<VAR>hgg' : ∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x<GOAL>∃ c ∈ Set.Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>g g' : ℝ → ℝ<VAR>lfa lga lfb lgb : ℝ<VAR>hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x<VAR>hfa : Filter.Tendsto f (𝓝[>] a) (𝓝 lfa)<VAR>hga : Filter.Tendsto g (𝓝[>] a) (𝓝 lga)<VAR>hfb : Filter.Tendsto f (𝓝[<] b) (𝓝 lfb)<VAR>hgb : Filter.Tendsto g (𝓝[<] b) (𝓝 lgb)<GOAL>∃ c ∈ Set.Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Set.Icc a b)<VAR>hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x<GOAL>∃ c ∈ Set.Ioo a b, f' c = (f b - f a) / (b - a)
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Set.Icc a b)<VAR>hfd : DifferentiableOn ℝ f (Set.Ioo a b)<VAR>g : ℝ → ℝ<VAR>hgc : ContinuousOn g (Set.Icc a b)<VAR>hgd : DifferentiableOn ℝ g (Set.Ioo a b)<GOAL>∃ c ∈ Set.Ioo a b, (g b - g a) * deriv f c = (f b - f a) * deriv g c
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>g : ℝ → ℝ<VAR>lfa lga lfb lgb : ℝ<VAR>hdf : DifferentiableOn ℝ f (Set.Ioo a b)<VAR>hdg : DifferentiableOn ℝ g (Set.Ioo a b)<VAR>hfa : Filter.Tendsto f (𝓝[>] a) (𝓝 lfa)<VAR>hga : Filter.Tendsto g (𝓝[>] a) (𝓝 lga)<VAR>hfb : Filter.Tendsto f (𝓝[<] b) (𝓝 lfb)<VAR>hgb : Filter.Tendsto g (𝓝[<] b) (𝓝 lgb)<GOAL>∃ c ∈ Set.Ioo a b, (lgb - lga) * deriv f c = (lfb - lfa) * deriv g c
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Set.Icc a b)<VAR>hfd : DifferentiableOn ℝ f (Set.Ioo a b)<GOAL>∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a)