ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>x : ℝ<GOAL>|x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) 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>f : SchwartzMap E F<VAR>n : ℕ<VAR>x₀ : E<GOAL>‖iteratedFDeriv ℝ n (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) 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>f : SchwartzMap E F<VAR>k : ℕ<VAR>x₀ : E<GOAL>‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) 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>f : SchwartzMap E F<VAR>x₀ : E<GOAL>‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) 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>n k : ℕ<GOAL>schwartzSeminormFamily 𝕜 E F (n, k) = SchwartzMap.seminorm 𝕜 n k
<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<GOAL>schwartzSeminormFamily 𝕜 E F 0 = SchwartzMap.seminorm 𝕜 0 0
<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>m : ℕ × ℕ<VAR>k n : ℕ<VAR>hk : k ≤ m.1<VAR>hn : n ≤ m.2<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>(1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ 2 ^ m.1 * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) 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<GOAL>WithSeminorms (schwartzSeminormFamily 𝕜 E 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 : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f<VAR>n : ℕ<GOAL>∃ k C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖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 : E → F<VAR>h'f : Function.HasTemperateGrowth (fderiv ℝ f)<VAR>hf : Differentiable ℝ f<VAR>k : ℕ<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k<GOAL>Function.HasTemperateGrowth f
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<GOAL>Function.HasTemperateGrowth fun 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>c : F<GOAL>Function.HasTemperateGrowth fun 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 : E →L[ℝ] F<GOAL>Function.HasTemperateGrowth ⇑f
<VAR>D : Type u_3<VAR>NormedAddCommGroup D<VAR>MeasurableSpace D<VAR>μ : MeasureTheory.Measure D<VAR>self : μ.HasTemperateGrowth<GOAL>∃ n, MeasureTheory.Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) μ
<VAR>D : Type u_3<VAR>NormedAddCommGroup D<VAR>MeasurableSpace D<VAR>μ : MeasureTheory.Measure D<VAR>h : μ.HasTemperateGrowth<GOAL>MeasureTheory.Integrable (fun x => (1 + ‖x‖) ^ (-↑μ.integrablePower)) μ
<VAR>C₁ C₂ : ℝ<VAR>k l : ℕ<VAR>x f : ℝ<VAR>hx : 0 ≤ x<VAR>hf : 0 ≤ f<VAR>h₁ : f ≤ C₁<VAR>h₂ : x ^ (k + l) * f ≤ C₂<GOAL>x ^ k * f ≤ 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l)
<VAR>D : Type u_3<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup D<VAR>MeasurableSpace D<VAR>BorelSpace D<VAR>SecondCountableTopology D<VAR>μ : MeasureTheory.Measure D<VAR>μ.HasTemperateGrowth<VAR>f : D → E<VAR>C₁ C₂ : ℝ<VAR>k : ℕ<VAR>hf : ∀ (x : D), ‖f x‖ ≤ C₁<VAR>h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂<VAR>h''f : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.Integrable (fun x => ‖x‖ ^ k * ‖f x‖) μ
<VAR>D : Type u_3<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup D<VAR>MeasurableSpace D<VAR>μ : MeasureTheory.Measure D<VAR>μ.HasTemperateGrowth<VAR>f : D → E<VAR>C₁ C₂ : ℝ<VAR>k : ℕ<VAR>hf : ∀ (x : D), ‖f x‖ ≤ C₁<VAR>h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂<GOAL>∫ (x : D), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ (2 ^ μ.integrablePower * ∫ (x : D), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) * (C₁ + C₂)
<VAR>𝕜 : Type u_1<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>RCLike 𝕜<VAR>NormedAddCommGroup D<VAR>NormedSpace ℝ D<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>g : D → E<VAR>hg : Function.HasTemperateGrowth g<VAR>hg_upper : ∃ k C, ∀ (x : D), ‖x‖ ≤ C * (1 + ‖g x‖) ^ k<VAR>f : SchwartzMap E F<GOAL>⇑((SchwartzMap.compCLM 𝕜 hg hg_upper) f) = ⇑f ∘ g
<VAR>𝕜 : Type u_1<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>RCLike 𝕜<VAR>NormedAddCommGroup D<VAR>NormedSpace ℝ D<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>K : ℝ≥0<VAR>g : D → E<VAR>hg : Function.HasTemperateGrowth g<VAR>h'g : AntilipschitzWith K g<VAR>f : SchwartzMap E F<GOAL>⇑((SchwartzMap.compCLMOfAntilipschitz 𝕜 hg h'g) f) = ⇑f ∘ g
<VAR>𝕜 : Type u_1<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>RCLike 𝕜<VAR>NormedAddCommGroup D<VAR>NormedSpace ℝ D<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>g : D ≃L[ℝ] E<VAR>f : SchwartzMap E F<GOAL>⇑((SchwartzMap.compCLMOfContinuousLinearEquiv 𝕜 g) f) = ⇑f ∘ ⇑g
<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>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>((SchwartzMap.fderivCLM 𝕜) f) x = fderiv ℝ (⇑f) x
<VAR>𝕜 : Type u_1<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>f : SchwartzMap ℝ F<VAR>x : ℝ<GOAL>((SchwartzMap.derivCLM 𝕜) f) x = deriv (⇑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>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>m : E<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>((SchwartzMap.pderivCLM 𝕜 m) f) x = (fderiv ℝ (⇑f) x) 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>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>m : E<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>((SchwartzMap.pderivCLM 𝕜 m) f) x = lineDeriv ℝ (⇑f) x 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>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>m : Fin 0 → E<VAR>f : SchwartzMap E F<GOAL>(SchwartzMap.iteratedPDeriv 𝕜 m) f = 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>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>m : Fin 1 → E<VAR>f : SchwartzMap E F<GOAL>(SchwartzMap.iteratedPDeriv 𝕜 m) f = (SchwartzMap.pderivCLM 𝕜 (m 0)) 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>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>n : ℕ<VAR>m : Fin (n + 1) → E<VAR>f : SchwartzMap E F<GOAL>(SchwartzMap.iteratedPDeriv 𝕜 m) f = (SchwartzMap.pderivCLM 𝕜 (m 0)) ((SchwartzMap.iteratedPDeriv 𝕜 (Fin.tail m)) 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>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>n : ℕ<VAR>m : Fin (n + 1) → E<VAR>f : SchwartzMap E F<GOAL>(SchwartzMap.iteratedPDeriv 𝕜 m) f = (SchwartzMap.iteratedPDeriv 𝕜 (Fin.init m)) ((SchwartzMap.pderivCLM 𝕜 (m (Fin.last n))) 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>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>n : ℕ<VAR>m : Fin n → E<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>((SchwartzMap.iteratedPDeriv 𝕜 m) f) x = (iteratedFDeriv ℝ n (⇑f) x) m
<VAR>D : Type u_3<VAR>V : Type u_7<VAR>NormedAddCommGroup D<VAR>NormedSpace ℝ D<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MeasurableSpace D<VAR>BorelSpace D<VAR>SecondCountableTopology D<VAR>μ : MeasureTheory.Measure D<VAR>hμ : μ.HasTemperateGrowth<VAR>f : SchwartzMap D V<VAR>k n : ℕ<GOAL>MeasureTheory.Integrable (fun x => ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖) μ
<VAR>D : Type u_3<VAR>V : Type u_7<VAR>NormedAddCommGroup D<VAR>NormedSpace ℝ D<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MeasurableSpace D<VAR>BorelSpace D<VAR>SecondCountableTopology D<VAR>μ : MeasureTheory.Measure D<VAR>hμ : μ.HasTemperateGrowth<VAR>f : SchwartzMap D V<VAR>k : ℕ<GOAL>MeasureTheory.Integrable (fun x => ‖x‖ ^ k * ‖f x‖) μ
<VAR>𝕜 : Type u_1<VAR>D : Type u_3<VAR>V : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup D<VAR>NormedSpace ℝ D<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedSpace 𝕜 V<VAR>MeasurableSpace D<VAR>μ : MeasureTheory.Measure D<VAR>hμ : μ.HasTemperateGrowth<VAR>f : SchwartzMap D V<VAR>k n : ℕ<GOAL>∫ (x : D), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ∂μ ≤ (2 ^ μ.integrablePower * ∫ (x : D), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) * ((SchwartzMap.seminorm 𝕜 0 n) f + (SchwartzMap.seminorm 𝕜 (k + μ.integrablePower) n) f)
<VAR>D : Type u_3<VAR>V : Type u_7<VAR>NormedAddCommGroup D<VAR>NormedSpace ℝ D<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MeasurableSpace D<VAR>BorelSpace D<VAR>SecondCountableTopology D<VAR>μ : MeasureTheory.Measure D<VAR>hμ : μ.HasTemperateGrowth<VAR>f : SchwartzMap D V<GOAL>MeasureTheory.Integrable (⇑f) μ
<VAR>𝕜 : Type u_1<VAR>D : Type u_3<VAR>V : Type u_7<VAR>RCLike 𝕜<VAR>NormedAddCommGroup D<VAR>NormedSpace ℝ D<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>NormedSpace 𝕜 V<VAR>MeasurableSpace D<VAR>BorelSpace D<VAR>SecondCountableTopology D<VAR>μ : MeasureTheory.Measure D<VAR>hμ : μ.HasTemperateGrowth<VAR>f : SchwartzMap D V<GOAL>(SchwartzMap.integralCLM 𝕜 μ) f = ∫ (x : D), 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 : SchwartzMap E F<VAR>x : E<GOAL>f.toBoundedContinuousFunction x = 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>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>((SchwartzMap.toBoundedContinuousFunctionCLM 𝕜 E F) f) x = 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>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>x₀ : E<VAR>f : SchwartzMap E F<GOAL>(SchwartzMap.delta 𝕜 F x₀) f = 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>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>SecondCountableTopology E<VAR>CompleteSpace F<VAR>x : E<GOAL>SchwartzMap.integralCLM 𝕜 (MeasureTheory.Measure.dirac x) = SchwartzMap.delta 𝕜 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>ProperSpace E<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>f.toZeroAtInfty x = 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>ProperSpace E<VAR>f : SchwartzMap E F<GOAL>f.toZeroAtInfty.toBCF = f.toBoundedContinuousFunction
<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>ProperSpace E<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 F<VAR>SMulCommClass ℝ 𝕜 F<VAR>f : SchwartzMap E F<VAR>x : E<GOAL>((SchwartzMap.toZeroAtInftyCLM 𝕜 E F) f) x = f x
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>x : E<GOAL>x ∈ convexJoin 𝕜 s t ↔ ∃ a ∈ s, ∃ b ∈ t, x ∈ segment 𝕜 a b
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<GOAL>convexJoin 𝕜 s t = convexJoin 𝕜 t s
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s₁ s₂ t₁ t₂ : Set E<VAR>hs : s₁ ⊆ s₂<VAR>ht : t₁ ⊆ t₂<GOAL>convexJoin 𝕜 s₁ t₁ ⊆ convexJoin 𝕜 s₂ t₂
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>t s₁ s₂ : Set E<VAR>hs : s₁ ⊆ s₂<GOAL>convexJoin 𝕜 s₁ t ⊆ convexJoin 𝕜 s₂ t
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t₁ t₂ : Set E<VAR>ht : t₁ ⊆ t₂<GOAL>convexJoin 𝕜 s t₁ ⊆ convexJoin 𝕜 s t₂
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>t : Set E<GOAL>convexJoin 𝕜 ∅ t = ∅
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<GOAL>convexJoin 𝕜 s ∅ = ∅
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>t : Set E<VAR>x : E<GOAL>convexJoin 𝕜 {x} t = ⋃ y ∈ t, segment 𝕜 x y
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>y : E<GOAL>convexJoin 𝕜 s {y} = ⋃ x ∈ s, segment 𝕜 x y
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>y : E<VAR>x : E<GOAL>convexJoin 𝕜 {x} {y} = segment 𝕜 x y
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s₁ s₂ t : Set E<GOAL>convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t₁ t₂ : Set E<GOAL>convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : ι → Set E<VAR>t : Set E<GOAL>convexJoin 𝕜 (⋃ i, s i) t = ⋃ i, convexJoin 𝕜 (s i) t
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>t : ι → Set E<GOAL>convexJoin 𝕜 s (⋃ i, t i) = ⋃ i, convexJoin 𝕜 s (t i)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ t<GOAL>segment 𝕜 x y ⊆ convexJoin 𝕜 s t
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>h : t.Nonempty<GOAL>s ⊆ convexJoin 𝕜 s t
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>h : s.Nonempty<GOAL>t ⊆ convexJoin 𝕜 s t
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t u : Set E<VAR>hs : s ⊆ u<VAR>ht : t ⊆ u<VAR>hu : Convex 𝕜 u<GOAL>convexJoin 𝕜 s t ⊆ u
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>OrderedSemiring 𝕜<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s t : Set E<GOAL>convexJoin 𝕜 s t ⊆ (convexHull 𝕜) (s ∪ t)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t u : Set E<GOAL>convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t u : Set E<GOAL>convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t u : Set E<GOAL>convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t u : Set E<GOAL>convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t u v : Set E<GOAL>convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<GOAL>Convex 𝕜 (convexJoin 𝕜 s t)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>hs₀ : s.Nonempty<VAR>ht₀ : t.Nonempty<GOAL>(convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 s t
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s t : Set E<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>(convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 ((convexHull 𝕜) s) ((convexHull 𝕜) t)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : s.Nonempty<GOAL>(convexHull 𝕜) (insert x s) = convexJoin 𝕜 {x} ((convexHull 𝕜) s)
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>a b c d : E<GOAL>convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜) {a, b, c, d}
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>a b c : E<GOAL>convexJoin 𝕜 (segment 𝕜 a b) {c} = (convexHull 𝕜) {a, b, c}
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>LinearOrderedField 𝕜<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>a b c : E<GOAL>convexJoin 𝕜 {a} (segment 𝕜 b c) = (convexHull 𝕜) {a, b, c}
<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>self : InnerProductSpace 𝕜 E<VAR>x y : E<VAR>r : 𝕜<GOAL>⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>self : InnerProductSpace 𝕜 E<VAR>x : E<GOAL>‖x‖ ^ 2 = RCLike.re ⟪x, x⟫_𝕜
<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>self : InnerProductSpace 𝕜 E<VAR>x y : E<GOAL>(starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>self : InnerProductSpace 𝕜 E<VAR>x y z : E<GOAL>⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜
<VAR>𝕜 : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>self : InnerProductSpace.Core 𝕜 F<VAR>x y : F<VAR>r : 𝕜<GOAL>⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>self : InnerProductSpace.Core 𝕜 F<VAR>x y z : F<GOAL>⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜
<VAR>𝕜 : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>self : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>0 ≤ RCLike.re ⟪x, x⟫_𝕜
<VAR>𝕜 : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>self : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>⟪x, x⟫_𝕜 = 0 → x = 0
<VAR>𝕜 : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>self : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>(starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>(starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>0 ≤ RCLike.re ⟪x, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>RCLike.im ⟪x, x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y z : F<GOAL>⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y z : F<GOAL>⟪x, y + z⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>↑(InnerProductSpace.Core.normSq x) = ⟪x, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>RCLike.re ⟪x, y⟫_𝕜 = RCLike.re ⟪y, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>RCLike.im ⟪x, y⟫_𝕜 = -RCLike.im ⟪y, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<VAR>r : 𝕜<GOAL>⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<VAR>r : 𝕜<GOAL>⟪x, r • y⟫_𝕜 = r * ⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>⟪0, x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>⟪x, 0⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>⟪x, x⟫_𝕜 = 0 ↔ x = 0
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>InnerProductSpace.Core.normSq x = 0 ↔ x = 0
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>⟪x, x⟫_𝕜 ≠ 0 ↔ x ≠ 0
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x : F<GOAL>↑(RCLike.re ⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>‖⟪x, y⟫_𝕜‖ = ‖⟪y, x⟫_𝕜‖
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>⟪x, -y⟫_𝕜 = -⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y z : F<GOAL>⟪x - y, z⟫_𝕜 = ⟪x, z⟫_𝕜 - ⟪y, z⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y z : F<GOAL>⟪x, y - z⟫_𝕜 = ⟪x, y⟫_𝕜 - ⟪x, z⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>RCLike.re (⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜) = ‖⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜‖
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>⟪x + y, x + y⟫_𝕜 = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>⟪x - y, x - y⟫_𝕜 = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>c : InnerProductSpace.Core 𝕜 F<VAR>x y : F<GOAL>InnerProductSpace.Core.normSq (⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y) = InnerProductSpace.Core.normSq x * (InnerProductSpace.Core.normSq x * InnerProductSpace.Core.normSq y - ‖⟪x, y⟫_𝕜‖ ^ 2)