ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → (ι → ℝ) → E<VAR>g : α → F<VAR>h : ∀ i ∈ s, BoxIntegral.HasIntegral I l (f i) vol (g i)<GOAL>BoxIntegral.HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y : F<VAR>hf : BoxIntegral.HasIntegral I l f vol y<VAR>c : ℝ<GOAL>BoxIntegral.HasIntegral I l (c • f) vol (c • y)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>hf : BoxIntegral.Integrable I l f vol<VAR>c : ℝ<GOAL>BoxIntegral.Integrable I l (c • f) vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>c : ℝ<VAR>hf : BoxIntegral.Integrable I l (c • f) vol<VAR>hc : c ≠ 0<GOAL>BoxIntegral.Integrable I l f vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>c : ℝ<GOAL>BoxIntegral.integral I l (fun x => c • f x) vol = c • BoxIntegral.integral I l f vol
<VAR>ι : Type u<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>g : (ι → ℝ) → ℝ<VAR>hg : ∀ x ∈ BoxIntegral.Box.Icc I, 0 ≤ g x<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>0 ≤ BoxIntegral.integral I l g μ.toBoxAdditive.toSMul
<VAR>ι : Type u<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>g : (ι → ℝ) → ℝ<VAR>hle : ∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ g x<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hg : BoxIntegral.Integrable I l g μ.toBoxAdditive.toSMul<GOAL>‖BoxIntegral.integral I l f μ.toBoxAdditive.toSMul‖ ≤ BoxIntegral.integral I l g μ.toBoxAdditive.toSMul
<VAR>ι : Type u<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>c : ℝ<VAR>hc : ∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ c<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>‖BoxIntegral.integral I l f μ.toBoxAdditive.toSMul‖ ≤ (μ ↑I).toReal * c
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>h : BoxIntegral.Integrable I l f vol<VAR>ε : ℝ<VAR>c : ℝ≥0<GOAL>l.RCond (h.convergenceR ε c)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>c : ℝ≥0<VAR>ε : ℝ<VAR>h : BoxIntegral.Integrable I l f vol<VAR>h₀ : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>hπp : π.IsPartition<GOAL>dist (BoxIntegral.integralSum f vol π) (BoxIntegral.integral I l f vol) ≤ ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>c₁ c₂ : ℝ≥0<VAR>ε₁ ε₂ : ℝ<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>h : BoxIntegral.Integrable I l f vol<VAR>hpos₁ : 0 < ε₁<VAR>hpos₂ : 0 < ε₂<VAR>h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁<VAR>h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂<VAR>HU : π₁.iUnion = π₂.iUnion<GOAL>dist (BoxIntegral.integralSum f vol π₁) (BoxIntegral.integralSum f vol π₂) ≤ ε₁ + ε₂
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>h : BoxIntegral.Integrable I l f vol<GOAL>Filter.Tendsto (fun π => (BoxIntegral.integralSum f vol π.1, BoxIntegral.integralSum f vol π.2)) (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 {π | π.1.iUnion = π.2.iUnion}) (𝓤 F)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>h : BoxIntegral.Integrable I l f vol<VAR>π₀ : BoxIntegral.Prepartition I<GOAL>Cauchy (Filter.map (BoxIntegral.integralSum f vol) (l.toFilteriUnion I π₀))
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I J : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>CompleteSpace F<VAR>h : BoxIntegral.Integrable I l f vol<VAR>hJ : J ≤ I<GOAL>∃ y, BoxIntegral.HasIntegral J l f vol y ∧ Filter.Tendsto (BoxIntegral.integralSum f vol) (l.toFilteriUnion I (BoxIntegral.Prepartition.single I J hJ)) (𝓝 y)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I J : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>CompleteSpace F<VAR>h : BoxIntegral.Integrable I l f vol<VAR>hJ : J ≤ I<GOAL>BoxIntegral.Integrable J l f vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I J : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>CompleteSpace F<VAR>h : BoxIntegral.Integrable I l f vol<VAR>hJ : J ≤ I<GOAL>Filter.Tendsto (BoxIntegral.integralSum f vol) (l.toFilteriUnion I (BoxIntegral.Prepartition.single I J hJ)) (𝓝 (BoxIntegral.integral J l f vol))
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>c : ℝ≥0<VAR>ε : ℝ<VAR>CompleteSpace F<VAR>h : BoxIntegral.Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : BoxIntegral.Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<GOAL>dist (BoxIntegral.integralSum f vol π) (∑ J ∈ π₀.boxes, BoxIntegral.integral J l f vol) ≤ ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>c : ℝ≥0<VAR>ε : ℝ<VAR>CompleteSpace F<VAR>h : BoxIntegral.Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<GOAL>dist (BoxIntegral.integralSum f vol π) (∑ J ∈ π.boxes, BoxIntegral.integral J l f vol) ≤ ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>CompleteSpace F<VAR>h : BoxIntegral.Integrable I l f vol<VAR>π₀ : BoxIntegral.Prepartition I<GOAL>Filter.Tendsto (BoxIntegral.integralSum f vol) (l.toFilteriUnion I π₀) (𝓝 (∑ J ∈ π₀.boxes, BoxIntegral.integral J l f vol))
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>CompleteSpace F<VAR>h : BoxIntegral.Integrable I l f vol<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>hU : π₁.iUnion = π₂.iUnion<GOAL>∑ J ∈ π₁.boxes, BoxIntegral.integral J l f vol = ∑ J ∈ π₂.boxes, BoxIntegral.integral J l f vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>CompleteSpace F<VAR>h : BoxIntegral.Integrable I l f vol<VAR>J : BoxIntegral.Box ι<GOAL>h.toBoxAdditive J = BoxIntegral.integral J l f vol
<VAR>ι : Type u<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>CompleteSpace E<VAR>I : BoxIntegral.Box ι<VAR>f : (ι → ℝ) → E<VAR>hb : ∃ C, ∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ C<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (BoxIntegral.Box.Icc I), ContinuousWithinAt f (BoxIntegral.Box.Icc I) x<GOAL>BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul
<VAR>ι : Type u<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>CompleteSpace E<VAR>I : BoxIntegral.Box ι<VAR>f : (ι → ℝ) → E<VAR>hb : ∃ C, ∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ C<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x<GOAL>BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul
<VAR>ι : Type u<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>CompleteSpace E<VAR>I : BoxIntegral.Box ι<VAR>f : (ι → ℝ) → E<VAR>hc : ContinuousOn f (BoxIntegral.Box.Icc I)<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : BoxIntegral.Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>H₁ : ∀ (c : ℝ≥0), ∀ x ∈ BoxIntegral.Box.Icc I ∩ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, BoxIntegral.Box.Icc J ⊆ Metric.closedBall x δ → x ∈ BoxIntegral.Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>H₂ : ∀ (c : ℝ≥0), ∀ x ∈ BoxIntegral.Box.Icc I \ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, BoxIntegral.Box.Icc J ⊆ Metric.closedBall x δ → (l.bHenstock = true → x ∈ BoxIntegral.Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<GOAL>BoxIntegral.HasIntegral I l f vol (g I)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>hl : l ≤ BoxIntegral.IntegrationParams.Henstock<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : BoxIntegral.Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>H₁ : ∀ (c : ℝ≥0), ∀ x ∈ BoxIntegral.Box.Icc I ∩ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, BoxIntegral.Box.Icc J ⊆ Metric.closedBall x δ → x ∈ BoxIntegral.Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>H₂ : ∀ (c : ℝ≥0), ∀ x ∈ BoxIntegral.Box.Icc I \ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, BoxIntegral.Box.Icc J ⊆ Metric.closedBall x δ → x ∈ BoxIntegral.Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<GOAL>BoxIntegral.HasIntegral I l f vol (g I)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : BoxIntegral.Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>H : ℝ≥0 → ∀ x ∈ BoxIntegral.Box.Icc I, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, BoxIntegral.Box.Icc J ⊆ Metric.closedBall x δ → dist ((vol J) (f x)) (g J) ≤ ε * B J<GOAL>BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.McShane f vol (g I)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedLinearOrderedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>self : StrictConvexSpace 𝕜 E<VAR>r : ℝ<GOAL>0 < r → StrictConvex 𝕜 (Metric.closedBall 0 r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedLinearOrderedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>StrictConvexSpace 𝕜 E<VAR>x : E<VAR>r : ℝ<GOAL>StrictConvex 𝕜 (Metric.closedBall x r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedLinearOrderedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>LinearMap.CompatibleSMul E E 𝕜 ℝ<VAR>h : StrictConvex 𝕜 (Metric.closedBall 0 1)<GOAL>StrictConvexSpace 𝕜 E
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1<GOAL>StrictConvexSpace ℝ E
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1<GOAL>StrictConvexSpace ℝ E
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2<GOAL>StrictConvexSpace ℝ E
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>h : (Metric.sphere 0 1).Pairwise fun x y => ‖x + y‖ ≠ 2<GOAL>StrictConvexSpace ℝ E
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y<GOAL>StrictConvexSpace ℝ E
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b r : ℝ<VAR>hx : x ∈ Metric.closedBall z r<VAR>hy : y ∈ Metric.closedBall z r<VAR>hne : x ≠ y<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ Metric.ball z r
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y z : E<VAR>r : ℝ<VAR>hx : x ∈ Metric.closedBall z r<VAR>hy : y ∈ Metric.closedBall z r<VAR>hne : x ≠ y<GOAL>openSegment ℝ x y ⊆ Metric.ball z r
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y : E<VAR>a b r : ℝ<VAR>hx : ‖x‖ ≤ r<VAR>hy : ‖y‖ ≤ r<VAR>hne : x ≠ y<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>‖a • x + b • y‖ < r
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y : E<VAR>h : ¬SameRay ℝ x y<GOAL>‖x + y‖ < ‖x‖ + ‖y‖
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y : E<VAR>h : ¬SameRay ℝ x y<GOAL>‖x‖ - ‖y‖ < ‖x - y‖
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y : E<VAR>h : ¬SameRay ℝ x y<GOAL>|‖x‖ - ‖y‖| < ‖x - y‖
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y : E<GOAL>SameRay ℝ x y ↔ ‖x + y‖ = ‖x‖ + ‖y‖
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y : E<VAR>h₁ : ‖x‖ = ‖y‖<VAR>h₂ : ‖x + y‖ = ‖x‖ + ‖y‖<GOAL>x = y
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y : E<GOAL>¬SameRay ℝ x y ↔ ‖x + y‖ < ‖x‖ + ‖y‖
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y : E<GOAL>SameRay ℝ x y ↔ ‖x - y‖ = |‖x‖ - ‖y‖|
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y : E<GOAL>¬SameRay ℝ x y ↔ |‖x‖ - ‖y‖| < ‖x - y‖
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x y : E<VAR>h : ‖x‖ = ‖y‖<GOAL>‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>self : SchwartzMap E F<GOAL>ContDiff ℝ ⊤ self.toFun
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>self : SchwartzMap E F<VAR>k n : ℕ<GOAL>∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n self.toFun x‖ ≤ C
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : SchwartzMap E F<VAR>k n : ℕ<GOAL>∃ C, 0 < C ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : SchwartzMap E F<VAR>n : ℕ∞<GOAL>ContDiff ℝ n ⇑f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : SchwartzMap E F<GOAL>Continuous ⇑f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : SchwartzMap E F<GOAL>Differentiable ℝ ⇑f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>DifferentiableAt ℝ (⇑f) x
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f g : SchwartzMap E F<VAR>h : ∀ (x : E), f x = g x<GOAL>f = g
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : SchwartzMap E F<VAR>k : ℕ<GOAL>⇑f =O[Filter.cocompact E] fun x => ‖x‖ ^ (-↑k)
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : SchwartzMap E F<VAR>ProperSpace E<VAR>s : ℝ<GOAL>⇑f =O[Filter.cocompact E] fun x => ‖x‖ ^ s
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : SchwartzMap E F<VAR>ProperSpace E<VAR>k : ℤ<GOAL>⇑f =O[Filter.cocompact E] fun x => ‖x‖ ^ k
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>k n : ℕ<VAR>f : SchwartzMap E F<GOAL>∃ c, c ∈ {c | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>k n : ℕ<VAR>f : SchwartzMap E F<GOAL>BddBelow {c | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>k n : ℕ<VAR>f g : SchwartzMap E F<VAR>x : E<GOAL>‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑g) x‖
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>k n : ℕ<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>‖x‖ ^ k * ‖iteratedFDeriv ℝ n (-⇑f) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>k n : ℕ<VAR>f : SchwartzMap E F<VAR>c : 𝕜<VAR>x : E<GOAL>‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>k n : ℕ<VAR>f : SchwartzMap E F<GOAL>0 ≤ SchwartzMap.seminormAux k n f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>k n : ℕ<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ SchwartzMap.seminormAux k n f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>k n : ℕ<VAR>f : SchwartzMap E F<VAR>M : ℝ<VAR>hMp : 0 ≤ M<VAR>hM : ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M<GOAL>SchwartzMap.seminormAux k n f ≤ M
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>f : SchwartzMap E F<VAR>c : 𝕜<VAR>x : E<GOAL>(c • f) x = c • f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>k n : ℕ<VAR>c : 𝕜<VAR>f : SchwartzMap E F<GOAL>SchwartzMap.seminormAux k n (c • f) ≤ ‖c‖ * SchwartzMap.seminormAux k n f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<GOAL>⇑0 = 0
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x : E<GOAL>0 x = 0
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>k n : ℕ<GOAL>SchwartzMap.seminormAux k n 0 = 0
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f g : SchwartzMap E F<VAR>x : E<GOAL>(f + g) x = f x + g x
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>k n : ℕ<VAR>f g : SchwartzMap E F<GOAL>SchwartzMap.seminormAux k n (f + g) ≤ SchwartzMap.seminormAux k n f + SchwartzMap.seminormAux k n g
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f g : SchwartzMap E F<VAR>x : E<GOAL>(f - g) x = f x - g x
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<GOAL>⇑(SchwartzMap.coeHom E F) = DFunLike.coe
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<GOAL>Function.Injective ⇑(SchwartzMap.coeHom E F)
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>k n : ℕ<VAR>f : SchwartzMap E F<VAR>M : ℝ<VAR>hMp : 0 ≤ M<VAR>hM : ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M<GOAL>(SchwartzMap.seminorm 𝕜 k n) f ≤ M
<VAR>𝕜 : Type u_1<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>k n : ℕ<VAR>f : SchwartzMap ℝ F<VAR>M : ℝ<VAR>hMp : 0 ≤ M<VAR>hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M<GOAL>(SchwartzMap.seminorm 𝕜 k n) f ≤ M
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>k n : ℕ<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f