ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R T<VAR>ι κ : Type w<VAR>inst✝¹ : Fintype ι<VAR>b✝ : Basis ι R S<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R S<VAR>s : S<GOAL>((toMatrix b b) ((lmul R S) s)).trace = ((toMatrix b b) (mulLeft R s)).trace
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>I : Box ι<VAR>s : Finset (ι × ℝ)<VAR>p : ι × ℝ<GOAL>splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ 0<VAR>hb : b ≠ ⊤<VAR>n : ℕ<VAR>hn : b / a < ↑n<GOAL>b < ↑n * a
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c a' b' c' : P<VAR>r : ℝ<VAR>h : ∠ a' b' c' = ∠ a b c<VAR>hab : dist a' b' = r * dist a b<VAR>hcb : dist c' b' = r * dist c b<GOAL>dist a' c' = r * dist a c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c a' b' c' : P<VAR>r : ℝ<VAR>h : ∠ a' b' c' = ∠ a b c<VAR>hab : dist a' b' = r * dist a b<VAR>hcb : dist c' b' = r * dist c b<VAR>h' : dist a' c' ^ 2 = (r * dist a c) ^ 2<GOAL>dist a' c' = r * dist a c
<VAR>α : Type u_1<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>a : α<GOAL>sign 0 = 0
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<GOAL>Tendsto (fun w => ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) (cocompact V) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∀ᶠ (x : V) in cocompact V, ‖∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • f v‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<GOAL>∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<GOAL>∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<GOAL>∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<GOAL>∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<GOAL>∃ T, ∀ (w : V), T ≤ ‖w‖ → ‖∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<GOAL>‖∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<GOAL>‖∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<GOAL>‖∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this : ‖1 / 2‖ = 2⁻¹<GOAL>‖∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this : ‖1 / 2‖ = 2⁻¹<GOAL>‖∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • (f v - f (v + i w))‖ < 2 * ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this : ‖1 / 2‖ = 2⁻¹<GOAL>∫ (a : V), ‖𝐞 (-⟪a, w⟫_ℝ) • (f a - f (a + i w))‖ < 2 * ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this : ‖1 / 2‖ = 2⁻¹<GOAL>∫ (a : V), ‖f a - f (a + (1 / (2 * ‖w‖ ^ 2)) • w)‖ < 2 * ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this : ‖1 / 2‖ = 2⁻¹<GOAL>∫ (v : V) in A, ‖f v - f (v + i w)‖ < 2 * ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this : ‖1 / 2‖ = 2⁻¹<VAR>bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B<GOAL>∫ (v : V) in A, ‖f v - f (v + i w)‖ < 2 * ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this : ‖1 / 2‖ = 2⁻¹<VAR>bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B<VAR>bdA2 : ‖∫ (x : V) in A, ‖f x - f (x + i w)‖‖ ≤ ε / ↑B * (volume A).toReal<GOAL>∫ (v : V) in A, ‖f v - f (v + i w)‖ < 2 * ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this : ‖1 / 2‖ = 2⁻¹<VAR>bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B<GOAL>AEStronglyMeasurable (fun x => ‖f x - f (x + i w)‖) (volume.restrict A)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this✝ : ‖1 / 2‖ = 2⁻¹<VAR>bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B<VAR>bdA2 : ‖∫ (x : V) in A, ‖f x - f (x + i w)‖‖ ≤ ε / ↑B * (volume A).toReal<VAR>this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖<GOAL>∫ (v : V) in A, ‖f v - f (v + i w)‖ < 2 * ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this✝ : ‖1 / 2‖ = 2⁻¹<VAR>bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B<VAR>bdA2 : ∫ (v : V) in A, ‖f v - f (v + i w)‖ ≤ ε / ↑B * (volume A).toReal<VAR>this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖<GOAL>ε / ↑B * (volume A).toReal < 2 * ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this✝ : ‖1 / 2‖ = 2⁻¹<VAR>bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B<VAR>bdA2 : ∫ (v : V) in A, ‖f v - f (v + i w)‖ ≤ ε / ↑B * (volume A).toReal<VAR>this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖<GOAL>(volume A).toReal < 2 * ↑B
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : (volume A).toReal ≤ (↑B).toReal<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this✝ : ‖1 / 2‖ = 2⁻¹<VAR>bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B<VAR>bdA2 : ∫ (v : V) in A, ‖f v - f (v + i w)‖ ≤ ε / ↑B * (volume A).toReal<VAR>this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖<GOAL>(volume A).toReal < 2 * ↑B
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this✝ : ‖1 / 2‖ = 2⁻¹<VAR>bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B<VAR>bdA2 : ∫ (v : V) in A, ‖f v - f (v + i w)‖ ≤ ε / ↑B * (volume A).toReal<VAR>this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖<GOAL>volume A ≠ ⊤
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hf1 : Continuous f<VAR>hf2 : HasCompactSupport f<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>R : ℝ<VAR>hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0<VAR>A : Set V := {v | ‖v‖ ≤ R + 1}<VAR>mA : MeasurableSet A<VAR>B : ℝ≥0<VAR>hB_pos : 0 < B<VAR>hB_vol : volume A ≤ ↑B<VAR>δ : ℝ<VAR>hδ1 : δ > 0<VAR>hδ2 : ∀ {a b : V}, dist a b < δ → dist (f a) (f b) < ε / ↑B<VAR>w : V<VAR>hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖<VAR>hw_ne : w ≠ 0<VAR>hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)<VAR>this✝ : ‖1 / 2‖ = 2⁻¹<VAR>bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B<VAR>bdA2 : ∫ (v : V) in A, ‖f v - f (v + i w)‖ ≤ ε / ↑B * (volume A).toReal<VAR>this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖<GOAL>↑B ≠ ⊤
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>j : J<GOAL>ι f j ≫ (isoCoproduct f).hom = ι f j ≫ desc (Sigma.ι f)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : AddGroup G<VAR>inst✝⁴ : AddTorsor G P<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : PreconnectedSpace G<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : ContinuousVAdd G P<GOAL>IsPreconnected Set.univ
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : AddGroup G<VAR>inst✝⁴ : AddTorsor G P<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : PreconnectedSpace G<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : ContinuousVAdd G P<GOAL>Set.univ = ⇑(Equiv.vaddConst (Classical.arbitrary P)) '' Set.univ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ s : Set E<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<GOAL>a • balancedHull 𝕜 s ⊆ balancedHull 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ s : Set E<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<GOAL>∀ (x : E), (∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ a • i • s) → ∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ s : Set E<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>x : E<VAR>r : 𝕜<VAR>hr : ‖r‖ ≤ 1<VAR>hx : x ∈ a • r • s<GOAL>∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ s : Set E<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>x : E<VAR>r : 𝕜<VAR>hr : ‖r‖ ≤ 1<VAR>hx : x ∈ (a • r) • s<GOAL>∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s
<VAR>r✝ : ℝ≥0<VAR>r : ℝ := ↑r✝<GOAL>HasSum (fun n => rexp (-↑r✝) * ↑r✝ ^ n / ↑n !) 1
<VAR>r✝ : ℝ≥0<VAR>r : ℝ := ↑r✝<GOAL>HasSum (fun i => rexp r * (rexp (-↑r✝) * ↑r✝ ^ i / ↑i !)) (rexp r * 1)
<VAR>r✝ : ℝ≥0<VAR>r : ℝ := ↑r✝<GOAL>HasSum (fun i => rexp r * (rexp (-↑r✝) * ↑r✝ ^ i / ↑i !)) (rexp r)
<VAR>r✝ : ℝ≥0<VAR>r : ℝ := ↑r✝<VAR>this : (fun i => rexp r * (rexp (-r) * r ^ i / ↑i !)) = fun i => r ^ i / ↑i !<GOAL>HasSum (fun i => rexp r * (rexp (-↑r✝) * ↑r✝ ^ i / ↑i !)) (rexp r)
<VAR>r✝ : ℝ≥0<VAR>r : ℝ := ↑r✝<VAR>this : (fun i => rexp r * (rexp (-r) * r ^ i / ↑i !)) = fun i => r ^ i / ↑i !<GOAL>HasSum (fun i => r ^ i / ↑i !) (NormedSpace.exp ℝ r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x✝ x y : α<GOAL>(y :: l).formPerm x = y ↔ (y :: l).formPerm x = (y :: l).formPerm ((y :: l).getLast ⋯)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>X Y : Mon_ C<VAR>P Q : Bimod X Y<VAR>f : P.X ≅ Q.X<VAR>f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft<VAR>f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight<GOAL>Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>X Y : Mon_ C<VAR>P Q : Bimod X Y<VAR>f : P.X ≅ Q.X<VAR>f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft<VAR>f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight<GOAL>Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight