ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace β<VAR>LinearOrderedCancelAddCommMonoid β<VAR>OrderTopology β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r s : β<GOAL>StrictConvex 𝕜 (Set.Icc r s)
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace β<VAR>LinearOrderedCancelAddCommMonoid β<VAR>OrderTopology β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r s : β<GOAL>StrictConvex 𝕜 (Set.Ioo r s)
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace β<VAR>LinearOrderedCancelAddCommMonoid β<VAR>OrderTopology β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r s : β<GOAL>StrictConvex 𝕜 (Set.Ico r s)
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace β<VAR>LinearOrderedCancelAddCommMonoid β<VAR>OrderTopology β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r s : β<GOAL>StrictConvex 𝕜 (Set.Ioc r s)
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace β<VAR>LinearOrderedCancelAddCommMonoid β<VAR>OrderTopology β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r s : β<GOAL>StrictConvex 𝕜 (Set.uIcc r s)
<VAR>𝕜 : Type u_1<VAR>β : Type u_5<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace β<VAR>LinearOrderedCancelAddCommMonoid β<VAR>OrderTopology β<VAR>Module 𝕜 β<VAR>OrderedSMul 𝕜 β<VAR>r s : β<GOAL>StrictConvex 𝕜 (Ι r s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCancelCommMonoid E<VAR>ContinuousAdd E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>z : E<GOAL>StrictConvex 𝕜 ((fun x => z + x) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCancelCommMonoid E<VAR>ContinuousAdd E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>z : E<GOAL>StrictConvex 𝕜 ((fun x => x + z) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ContinuousAdd E<VAR>s t : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>ht : StrictConvex 𝕜 t<GOAL>StrictConvex 𝕜 (s + t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ContinuousAdd E<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>z : E<GOAL>StrictConvex 𝕜 ((fun x => z + x) '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ContinuousAdd E<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>z : E<GOAL>StrictConvex 𝕜 ((fun x => x + z) '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>ContinuousAdd E<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>x : E<GOAL>StrictConvex 𝕜 (x +ᵥ s)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>LinearOrderedField 𝕝<VAR>Module 𝕝 E<VAR>ContinuousConstSMul 𝕝 E<VAR>LinearMap.CompatibleSMul E E 𝕜 𝕝<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>c : 𝕝<GOAL>StrictConvex 𝕜 (c • s)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>LinearOrderedField 𝕝<VAR>Module 𝕝 E<VAR>ContinuousConstSMul 𝕝 E<VAR>LinearMap.CompatibleSMul E E 𝕜 𝕝<VAR>s : Set E<VAR>ContinuousAdd E<VAR>hs : StrictConvex 𝕜 s<VAR>z : E<VAR>c : 𝕝<GOAL>StrictConvex 𝕜 (z +ᵥ c • s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedCommSemiring 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>NoZeroSMulDivisors 𝕜 E<VAR>ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>c : 𝕜<GOAL>StrictConvex 𝕜 ((fun z => c • z) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedRing 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x y : E<VAR>Nontrivial 𝕜<VAR>DenselyOrdered 𝕜<VAR>hs : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>h : openSegment 𝕜 x y ⊆ frontier s<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedRing 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x y : E<VAR>hs : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hxy : x + y ∈ s<VAR>hy : y ≠ 0<VAR>t : 𝕜<VAR>ht₀ : 0 < t<VAR>ht₁ : t < 1<GOAL>x + t • y ∈ interior s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedRing 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : StrictConvex 𝕜 s<VAR>zero_mem : 0 ∈ s<VAR>hx : x ∈ s<VAR>hx₀ : x ≠ 0<VAR>t : 𝕜<VAR>ht₀ : 0 < t<VAR>ht₁ : t < 1<GOAL>t • x ∈ interior s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedRing 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x y : E<VAR>h : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>t : 𝕜<VAR>ht₀ : 0 < t<VAR>ht₁ : t < 1<GOAL>x + t • (y - x) ∈ interior s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>OrderedRing 𝕜<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set F<VAR>hs : StrictConvex 𝕜 s<VAR>f : E →ᵃ[𝕜] F<VAR>hf : Continuous ⇑f<VAR>hfinj : Function.Injective ⇑f<GOAL>StrictConvex 𝕜 (⇑f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>OrderedRing 𝕜<VAR>TopologicalSpace E<VAR>TopologicalSpace F<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>f : E →ᵃ[𝕜] F<VAR>hf : IsOpenMap ⇑f<GOAL>StrictConvex 𝕜 (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedRing 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>TopologicalAddGroup E<VAR>hs : StrictConvex 𝕜 s<GOAL>StrictConvex 𝕜 (-s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>OrderedRing 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>TopologicalAddGroup E<VAR>hs : StrictConvex 𝕜 s<VAR>ht : StrictConvex 𝕜 t<GOAL>StrictConvex 𝕜 (s - t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>StrictConvex 𝕜 s ↔ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
<VAR>𝕜 : Type u_1<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : StrictConvex 𝕜 s<VAR>zero_mem : 0 ∈ s<VAR>hx : x ∈ s<VAR>hx₀ : x ≠ 0<VAR>t : 𝕜<VAR>ht : 1 < t<GOAL>x ∈ t • interior s
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>s : Set 𝕜<GOAL>StrictConvex 𝕜 s ↔ Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>s : Set 𝕜<GOAL>StrictConvex 𝕜 s ↔ s.OrdConnected
<VAR>x : ℂ<VAR>h : Complex.cos x ≠ 0<GOAL>HasStrictDerivAt Complex.tan (1 / Complex.cos x ^ 2) x
<VAR>x : ℂ<VAR>h : Complex.cos x ≠ 0<GOAL>HasDerivAt Complex.tan (1 / Complex.cos x ^ 2) x
<VAR>x : ℂ<VAR>hx : Complex.cos x = 0<GOAL>Filter.Tendsto (fun x => Complex.abs (Complex.tan x)) (nhdsWithin x {x}ᶜ) Filter.atTop
<VAR>k : ℤ<GOAL>Filter.Tendsto (fun x => Complex.abs (Complex.tan x)) (nhdsWithin ((2 * ↑k + 1) * ↑Real.pi / 2) {(2 * ↑k + 1) * ↑Real.pi / 2}ᶜ) Filter.atTop
<VAR>x : ℂ<GOAL>ContinuousAt Complex.tan x ↔ Complex.cos x ≠ 0
<VAR>x : ℂ<GOAL>DifferentiableAt ℂ Complex.tan x ↔ Complex.cos x ≠ 0
<VAR>x : ℂ<GOAL>deriv Complex.tan x = 1 / Complex.cos x ^ 2
<VAR>x : ℂ<VAR>n : ℕ∞<GOAL>ContDiffAt ℂ n Complex.tan x ↔ Complex.cos x ≠ 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : ι → E<VAR>h : ¬AffineIndependent 𝕜 f<GOAL>∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>F : ι → Set E<VAR>s : Finset ι<VAR>h_card_small : s.card ≤ FiniteDimensional.finrank 𝕜 E + 1<VAR>h_inter : ∀ I ⊆ s, I.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<GOAL>(⋂ i ∈ s, F i).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>F : ι → Set E<VAR>s : Finset ι<VAR>h_convex : ∀ i ∈ s, Convex 𝕜 (F i)<VAR>h_inter : ∀ I ⊆ s, I.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<GOAL>(⋂ i ∈ s, F i).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>F : ι → Set E<VAR>s : Finset ι<VAR>h_card : FiniteDimensional.finrank 𝕜 E + 1 ≤ s.card<VAR>h_convex : ∀ i ∈ s, Convex 𝕜 (F i)<VAR>h_inter : ∀ I ⊆ s, I.card = FiniteDimensional.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<GOAL>(⋂ i ∈ s, F i).Nonempty
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>F : Finset (Set E)<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_inter : ∀ G ⊆ F, G.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<GOAL>(⋂₀ ↑F).Nonempty
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>F : Finset (Set E)<VAR>h_card : FiniteDimensional.finrank 𝕜 E + 1 ≤ F.card<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_inter : ∀ G ⊆ F, G.card = FiniteDimensional.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<GOAL>(⋂₀ ↑F).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>F : ι → Set E<VAR>h_convex : ∀ (i : ι), Convex 𝕜 (F i)<VAR>h_compact : ∀ (i : ι), IsCompact (F i)<VAR>h_inter : ∀ (I : Finset ι), I.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<GOAL>(⋂ i, F i).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>F : ι → Set E<VAR>h_card : ↑(FiniteDimensional.finrank 𝕜 E) + 1 ≤ PartENat.card ι<VAR>h_convex : ∀ (i : ι), Convex 𝕜 (F i)<VAR>h_compact : ∀ (i : ι), IsCompact (F i)<VAR>h_inter : ∀ (I : Finset ι), I.card = FiniteDimensional.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<GOAL>(⋂ i, F i).Nonempty
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>F : Set (Set E)<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_compact : ∀ X ∈ F, IsCompact X<VAR>h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<GOAL>(⋂₀ F).Nonempty
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>F : Set (Set E)<VAR>h_card : ↑(FiniteDimensional.finrank 𝕜 E) + 1 ≤ F.encard<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_compact : ∀ X ∈ F, IsCompact X<VAR>h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card = FiniteDimensional.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<GOAL>(⋂₀ F).Nonempty
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>v : ℝ → E → E<VAR>tMin t₀ tMax : ℝ<VAR>x₀ : E<VAR>L : ℝ≥0<VAR>R C : ℝ<VAR>self : IsPicardLindelof v tMin t₀ tMax x₀ L R C<VAR>t : ℝ<GOAL>t ∈ Set.Icc tMin tMax → ∀ x ∈ Metric.closedBall x₀ R, ‖v t x‖ ≤ C
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>v : ℝ → E → E<VAR>tMin t₀ tMax : ℝ<VAR>x₀ : E<VAR>L : ℝ≥0<VAR>R C : ℝ<VAR>self : IsPicardLindelof v tMin t₀ tMax x₀ L R C<VAR>t : ℝ<GOAL>t ∈ Set.Icc tMin tMax → LipschitzOnWith L (v t) (Metric.closedBall x₀ R)
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>v : ℝ → E → E<VAR>tMin t₀ tMax : ℝ<VAR>x₀ : E<VAR>L : ℝ≥0<VAR>R C : ℝ<VAR>self : IsPicardLindelof v tMin t₀ tMax x₀ L R C<GOAL>t₀ ∈ Set.Icc tMin tMax
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>v : ℝ → E → E<VAR>tMin t₀ tMax : ℝ<VAR>x₀ : E<VAR>L : ℝ≥0<VAR>R C : ℝ<VAR>self : IsPicardLindelof v tMin t₀ tMax x₀ L R C<GOAL>0 ≤ R
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>v : ℝ → E → E<VAR>tMin t₀ tMax : ℝ<VAR>x₀ : E<VAR>L : ℝ≥0<VAR>R C : ℝ<VAR>self : IsPicardLindelof v tMin t₀ tMax x₀ L R C<VAR>x : E<GOAL>x ∈ Metric.closedBall x₀ R → ContinuousOn (fun t => v t x) (Set.Icc tMin tMax)
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>v : ℝ → E → E<VAR>tMin t₀ tMax : ℝ<VAR>x₀ : E<VAR>L : ℝ≥0<VAR>R C : ℝ<VAR>self : IsPicardLindelof v tMin t₀ tMax x₀ L R C<GOAL>C * max (tMax - t₀) (t₀ - tMin) ≤ R
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>self : PicardLindelof E<GOAL>IsPicardLindelof self.toFun self.tMin (↑self.t₀) self.tMax self.x₀ self.L ↑self.R ↑self.C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<GOAL>v.tMin ≤ v.tMax
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<GOAL>(Set.Icc v.tMin v.tMax).Nonempty
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>t : ℝ<VAR>ht : t ∈ Set.Icc v.tMin v.tMax<GOAL>LipschitzOnWith v.L (v.toFun t) (Metric.closedBall v.x₀ ↑v.R)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<GOAL>ContinuousOn (Function.uncurry v.toFun) (Set.Icc v.tMin v.tMax ×ˢ Metric.closedBall v.x₀ ↑v.R)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>t : ℝ<VAR>ht : t ∈ Set.Icc v.tMin v.tMax<VAR>x : E<VAR>hx : x ∈ Metric.closedBall v.x₀ ↑v.R<GOAL>‖v.toFun t x‖ ≤ ↑v.C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<GOAL>0 ≤ v.tDist
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>t : ↑(Set.Icc v.tMin v.tMax)<GOAL>dist t v.t₀ ≤ v.tDist
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>t : ↑(Set.Icc v.tMin v.tMax)<GOAL>v.proj ↑t = t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>t : ℝ<VAR>ht : t ∈ Set.Icc v.tMin v.tMax<GOAL>↑(v.proj t) = t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<GOAL>Continuous v.proj
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>self : v.FunSpace<GOAL>LipschitzWith v.C self.toFun
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>self : v.FunSpace<GOAL>self.toFun v.t₀ = v.x₀
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<GOAL>LipschitzWith v.C f.toFun
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<GOAL>Continuous f.toFun
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<GOAL>UniformInducing ⇑PicardLindelof.FunSpace.toContinuousMap
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<GOAL>Set.range ⇑PicardLindelof.FunSpace.toContinuousMap = {f | f v.t₀ = v.x₀ ∧ LipschitzWith v.C ⇑f}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<GOAL>f.toFun v.t₀ = v.x₀
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>t : ↑(Set.Icc v.tMin v.tMax)<GOAL>f.toFun t ∈ Metric.closedBall v.x₀ ↑v.R
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>t : ↑(Set.Icc v.tMin v.tMax)<GOAL>f.vComp ↑t = v.toFun (↑t) (f.toFun t)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<GOAL>Continuous f.vComp
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>t : ℝ<GOAL>‖f.vComp t‖ ≤ ↑v.C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f₁ f₂ : v.FunSpace<VAR>t : ↑(Set.Icc v.tMin v.tMax)<GOAL>dist (f₁.toFun t) (f₂.toFun t) ≤ dist f₁ f₂
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f₁ f₂ : v.FunSpace<VAR>d : ℝ<VAR>h : ∀ (t : ↑(Set.Icc v.tMin v.tMax)), dist (f₁.toFun t) (f₂.toFun t) ≤ d<GOAL>dist f₁ f₂ ≤ d
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>t₁ t₂ : ℝ<GOAL>IntervalIntegrable f.vComp MeasureTheory.volume t₁ t₂
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>t : ↑(Set.Icc v.tMin v.tMax)<GOAL>f.next.toFun t = v.x₀ + ∫ (τ : ℝ) in ↑v.t₀..↑t, f.vComp τ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>CompleteSpace E<VAR>t : ↑(Set.Icc v.tMin v.tMax)<GOAL>HasDerivWithinAt (f.next.toFun ∘ v.proj) (v.toFun (↑t) (f.toFun t)) (Set.Icc v.tMin v.tMax) ↑t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f₁ f₂ : v.FunSpace<VAR>n : ℕ<VAR>d : ℝ<VAR>h : ∀ (t : ↑(Set.Icc v.tMin v.tMax)), dist (f₁.toFun t) (f₂.toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d<VAR>t : ↑(Set.Icc v.tMin v.tMax)<GOAL>dist (f₁.next.toFun t) (f₂.next.toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f₁ f₂ : v.FunSpace<VAR>n : ℕ<VAR>t : ↑(Set.Icc v.tMin v.tMax)<GOAL>dist ((PicardLindelof.FunSpace.next^[n] f₁).toFun t) ((PicardLindelof.FunSpace.next^[n] f₂).toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f₁ f₂ : v.FunSpace<VAR>n : ℕ<GOAL>dist (PicardLindelof.FunSpace.next^[n] f₁) (PicardLindelof.FunSpace.next^[n] f₂) ≤ (↑v.L * v.tDist) ^ n / ↑n ! * dist f₁ f₂
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<GOAL>∃ N K, ContractingWith K PicardLindelof.FunSpace.next^[N]
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>CompleteSpace E<GOAL>∃ f, f.next = f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>CompleteSpace E<GOAL>∃ f, f ↑v.t₀ = v.x₀ ∧ ∀ t ∈ Set.Icc v.tMin v.tMax, HasDerivWithinAt f (v.toFun t (f t)) (Set.Icc v.tMin v.tMax) t
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>v : ℝ → E → E<VAR>tMin t₀ tMax : ℝ<VAR>x₀ : E<VAR>C R : ℝ<VAR>L : ℝ≥0<VAR>hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C<GOAL>‖v t₀ x₀‖ ≤ C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>v : ℝ → E → E<VAR>tMin t₀ tMax : ℝ<VAR>x₀ : E<VAR>C R : ℝ<VAR>L : ℝ≥0<VAR>hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C<GOAL>∃ f, f t₀ = x₀ ∧ ∀ t ∈ Set.Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Set.Icc tMin tMax) t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>hv : ContDiffAt ℝ 1 v x₀<GOAL>∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>CompleteSpace E<VAR>hv : ContDiffAt ℝ 1 v x₀<GOAL>∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>CompleteSpace E<VAR>hv : ContDiff ℝ 1 v<GOAL>∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t
<VAR>z : ℂ<GOAL>HasSum (fun n => (z * Complex.I) ^ (2 * n) / ↑(2 * n)!) (Complex.cos z)
<VAR>z : ℂ<GOAL>HasSum (fun n => (z * Complex.I) ^ (2 * n + 1) / ↑(2 * n + 1)! / Complex.I) (Complex.sin z)
<VAR>z : ℂ<GOAL>HasSum (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) (Complex.cos z)
<VAR>z : ℂ<GOAL>HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) (Complex.sin z)
<VAR>z : ℂ<GOAL>Complex.cos z = ∑' (n : ℕ), (z * Complex.I) ^ (2 * n) / ↑(2 * n)!
<VAR>z : ℂ<GOAL>Complex.sin z = ∑' (n : ℕ), (z * Complex.I) ^ (2 * n + 1) / ↑(2 * n + 1)! / Complex.I
<VAR>z : ℂ<GOAL>Complex.cos z = ∑' (n : ℕ), (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!
<VAR>z : ℂ<GOAL>Complex.sin z = ∑' (n : ℕ), (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!
<VAR>r : ℝ<GOAL>HasSum (fun n => (-1) ^ n * r ^ (2 * n) / ↑(2 * n)!) (Real.cos r)
<VAR>r : ℝ<GOAL>HasSum (fun n => (-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1)!) (Real.sin r)
<VAR>r : ℝ<GOAL>Real.cos r = ∑' (n : ℕ), (-1) ^ n * r ^ (2 * n) / ↑(2 * n)!
<VAR>r : ℝ<GOAL>Real.sin r = ∑' (n : ℕ), (-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1)!
<VAR>z : ℂ<GOAL>HasSum (fun n => z ^ (2 * n) / ↑(2 * n)!) (Complex.cosh z)
<VAR>z : ℂ<GOAL>HasSum (fun n => z ^ (2 * n + 1) / ↑(2 * n + 1)!) (Complex.sinh z)
<VAR>z : ℂ<GOAL>Complex.cosh z = ∑' (n : ℕ), z ^ (2 * n) / ↑(2 * n)!
<VAR>z : ℂ<GOAL>Complex.sinh z = ∑' (n : ℕ), z ^ (2 * n + 1) / ↑(2 * n + 1)!
<VAR>r : ℝ<GOAL>HasSum (fun n => r ^ (2 * n) / ↑(2 * n)!) (Real.cosh r)
<VAR>r : ℝ<GOAL>HasSum (fun n => r ^ (2 * n + 1) / ↑(2 * n + 1)!) (Real.sinh r)
<VAR>r : ℝ<GOAL>Real.cosh r = ∑' (n : ℕ), r ^ (2 * n) / ↑(2 * n)!
<VAR>r : ℝ<GOAL>Real.sinh r = ∑' (n : ℕ), r ^ (2 * n + 1) / ↑(2 * n + 1)!
<VAR>x : ℝ<GOAL>Real.cosh x ≤ Real.exp (x ^ 2 / 2)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>f : C(α, 𝕜)<GOAL>NormedSpace.exp 𝕜 f = { toFun := NormedSpace.exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ }
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>RCLike 𝕜<VAR>p : A → Prop<VAR>NormedRing A<VAR>StarRing A<VAR>TopologicalRing A<VAR>NormedAlgebra 𝕜 A<VAR>CompleteSpace A<VAR>ContinuousFunctionalCalculus 𝕜 p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc (NormedSpace.exp 𝕜) a = NormedSpace.exp 𝕜 a
<VAR>A : Type u_1<VAR>p : A → Prop<VAR>NormedRing A<VAR>StarRing A<VAR>TopologicalRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>ContinuousFunctionalCalculus ℝ p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc Real.exp a = NormedSpace.exp ℝ a
<VAR>A : Type u_1<VAR>p : A → Prop<VAR>NormedRing A<VAR>StarRing A<VAR>TopologicalRing A<VAR>NormedAlgebra ℂ A<VAR>CompleteSpace A<VAR>ContinuousFunctionalCalculus ℂ p<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>cfc Complex.exp a = NormedSpace.exp ℂ a
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>NormedAlgebra ℝ A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>a : A<GOAL>IsSelfAdjoint (CFC.log a)
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>TopologicalRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>UniqueContinuousFunctionalCalculus ℝ A<VAR>a : A<VAR>ha : IsSelfAdjoint a := by cfc_tac<GOAL>CFC.log (NormedSpace.exp ℝ a) = a
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>TopologicalRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>UniqueContinuousFunctionalCalculus ℝ A<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>ha₁ : IsSelfAdjoint a := by cfc_tac<GOAL>NormedSpace.exp ℝ (CFC.log a) = a
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>NormedAlgebra ℝ A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<GOAL>CFC.log 0 = 0
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>NormedAlgebra ℝ A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<GOAL>CFC.log 1 = 0
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>NormedAlgebra ℝ A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>r : ℝ<GOAL>CFC.log ((algebraMap ℝ A) r) = (algebraMap ℝ A) (Real.log r)
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>NormedAlgebra ℝ A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>UniqueContinuousFunctionalCalculus ℝ A<VAR>r : ℝ<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>hr : 0 < r<VAR>ha₁ : IsSelfAdjoint a := by cfc_tac<GOAL>CFC.log (r • a) = (algebraMap ℝ A) (Real.log r) + CFC.log a
<VAR>A : Type u_1<VAR>NormedRing A<VAR>StarRing A<VAR>NormedAlgebra ℝ A<VAR>ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>UniqueContinuousFunctionalCalculus ℝ A<VAR>n : ℕ<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>ha₁ : IsSelfAdjoint a := by cfc_tac<GOAL>CFC.log (a ^ n) = n • CFC.log a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>x : A<VAR>n : ℤ<GOAL>(Polynomial.aeval x) (Polynomial.Chebyshev.T R n) = Polynomial.eval x (Polynomial.Chebyshev.T A n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>x : A<VAR>n : ℤ<GOAL>(Polynomial.aeval x) (Polynomial.Chebyshev.U R n) = Polynomial.eval x (Polynomial.Chebyshev.U A n)