ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>ha : IsCauSeq abs fun m => ∑ n ∈ range m, abv (f n)<VAR>hb : IsCauSeq abv fun m => ∑ n ∈ range m, g n<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>P : α<VAR>hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P<VAR>Q : α<VAR>hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q<VAR>hP0 : 0 < P<VAR>hPε0 : 0 < ε / (2 * P)<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)<VAR>hQε0 : 0 < ε / (4 * Q)<VAR>M : ℕ<VAR>hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)<VAR>K : ℕ<VAR>hK : K ≥ 2 * (max N M + 1)<VAR>h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n<VAR>h₂ : (fun i => ∑ k ∈ range (K - i), f i * g k) = fun i => f i * ∑ k ∈ range (K - i), g k<VAR>h₃ : ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k = ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k<VAR>two_mul_two : 4 = 2 * 2<VAR>hQ0 : Q ≠ 0<VAR>h2Q0 : 2 * Q ≠ 0<VAR>hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε<VAR>hNMK : max N M + 1 < K<VAR>hKN : N < K<VAR>hsumlesum : ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤ ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))<VAR>hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P<GOAL>abv (∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>ha : IsCauSeq abs fun m => ∑ n ∈ range m, abv (f n)<VAR>hb : IsCauSeq abv fun m => ∑ n ∈ range m, g n<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>P : α<VAR>hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P<VAR>Q : α<VAR>hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q<VAR>hP0 : 0 < P<VAR>hPε0 : 0 < ε / (2 * P)<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)<VAR>hQε0 : 0 < ε / (4 * Q)<VAR>M : ℕ<VAR>hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)<VAR>K : ℕ<VAR>hK : K ≥ 2 * (max N M + 1)<VAR>h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n<VAR>h₂ : (fun i => ∑ k ∈ range (K - i), f i * g k) = fun i => f i * ∑ k ∈ range (K - i), g k<VAR>h₃ : ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k = ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k<VAR>two_mul_two : 4 = 2 * 2<VAR>hQ0 : Q ≠ 0<VAR>h2Q0 : 2 * Q ≠ 0<VAR>hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε<VAR>hNMK : max N M + 1 < K<VAR>hKN : N < K<VAR>hsumlesum : ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤ ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))<VAR>hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P<GOAL>∑ i ∈ range K, abv (f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>ha : IsCauSeq abs fun m => ∑ n ∈ range m, abv (f n)<VAR>hb : IsCauSeq abv fun m => ∑ n ∈ range m, g n<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>P : α<VAR>hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P<VAR>Q : α<VAR>hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q<VAR>hP0 : 0 < P<VAR>hPε0 : 0 < ε / (2 * P)<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)<VAR>hQε0 : 0 < ε / (4 * Q)<VAR>M : ℕ<VAR>hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)<VAR>K : ℕ<VAR>hK : K ≥ 2 * (max N M + 1)<VAR>h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n<VAR>h₂ : (fun i => ∑ k ∈ range (K - i), f i * g k) = fun i => f i * ∑ k ∈ range (K - i), g k<VAR>h₃ : ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k = ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k<VAR>two_mul_two : 4 = 2 * 2<VAR>hQ0 : Q ≠ 0<VAR>h2Q0 : 2 * Q ≠ 0<VAR>hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε<VAR>hNMK : max N M + 1 < K<VAR>hKN : N < K<VAR>hsumlesum : ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤ ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))<VAR>hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P<GOAL>∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + (∑ i ∈ range K, abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) - ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) < ε / (2 * P) * P + ε / (4 * Q) * (2 * Q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>ha : IsCauSeq abs fun m => ∑ n ∈ range m, abv (f n)<VAR>hb : IsCauSeq abv fun m => ∑ n ∈ range m, g n<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>P : α<VAR>hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P<VAR>Q : α<VAR>hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q<VAR>hP0 : 0 < P<VAR>hPε0 : 0 < ε / (2 * P)<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)<VAR>hQε0 : 0 < ε / (4 * Q)<VAR>M : ℕ<VAR>hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)<VAR>K : ℕ<VAR>hK : K ≥ 2 * (max N M + 1)<VAR>h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n<VAR>h₂ : (fun i => ∑ k ∈ range (K - i), f i * g k) = fun i => f i * ∑ k ∈ range (K - i), g k<VAR>h₃ : ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k = ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k<VAR>two_mul_two : 4 = 2 * 2<VAR>hQ0 : Q ≠ 0<VAR>h2Q0 : 2 * Q ≠ 0<VAR>hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε<VAR>hNMK : max N M + 1 < K<VAR>hKN : N < K<VAR>hsumlesum : ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤ ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))<VAR>hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P<GOAL>∑ i ∈ range K, abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) - ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) < ε / (4 * Q) * (2 * Q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>ha : IsCauSeq abs fun m => ∑ n ∈ range m, abv (f n)<VAR>hb : IsCauSeq abv fun m => ∑ n ∈ range m, g n<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>P : α<VAR>hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P<VAR>Q : α<VAR>hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q<VAR>hP0 : 0 < P<VAR>hPε0 : 0 < ε / (2 * P)<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)<VAR>hQε0 : 0 < ε / (4 * Q)<VAR>M : ℕ<VAR>hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)<VAR>K : ℕ<VAR>hK : K ≥ 2 * (max N M + 1)<VAR>h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n<VAR>h₂ : (fun i => ∑ k ∈ range (K - i), f i * g k) = fun i => f i * ∑ k ∈ range (K - i), g k<VAR>h₃ : ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k = ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k<VAR>two_mul_two : 4 = 2 * 2<VAR>hQ0 : Q ≠ 0<VAR>h2Q0 : 2 * Q ≠ 0<VAR>hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε<VAR>hNMK : max N M + 1 < K<VAR>hKN : N < K<VAR>hsumlesum : ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤ ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))<VAR>hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P<GOAL>∑ k ∈ filter (fun k => max N M + 1 ≤ k) (range K), abv (f k) * abv (∑ k ∈ range (K - k), g k - ∑ k ∈ range K, g k) < ε / (4 * Q) * (2 * Q)
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>x • ball 1 δ = ball x δ
<VAR>Γ : Type u_1<VAR>inst✝⁵ : PartialOrder Γ<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>A : HVertexOperator Γ R V W<VAR>n : Γ<VAR>x✝¹ : R<VAR>x✝ : V<GOAL>{ toFun := fun v => ((of R).symm (A v)).coeff n, map_add' := ⋯ }.toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • { toFun := fun v => ((of R).symm (A v)).coeff n, map_add' := ⋯ }.toFun x✝
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.36964, u_1} D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>monomorphisms C f ↔ Mono f
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s✝ : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>f : ι → κ → G<VAR>s : Set κ<VAR>l : Filter ι<GOAL>UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun n z => f n.1 z / f n.2 z) 1 (l ×ˢ l) s
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<GOAL>yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>re_eq✝ : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im<VAR>h : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re<GOAL>yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<GOAL>∫ (x : E), lineDeriv ℝ f x v * g x ∂μ = ∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<VAR>A : Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))<GOAL>∫ (x : E), lineDeriv ℝ f x v * g x ∂μ = ∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<VAR>A : Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))<VAR>B : Tendsto (fun t => ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))<GOAL>∫ (x : E), lineDeriv ℝ f x v * g x ∂μ = ∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<VAR>A : Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))<VAR>B : Tendsto (fun t => ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))<GOAL>∀ (t : ℝ), ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ = ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<VAR>A : Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))<VAR>B : Tendsto (fun t => ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))<VAR>t : ℝ<GOAL>∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ = ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<VAR>A : Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))<VAR>B : Tendsto (fun t => ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))<VAR>t : ℝ<GOAL>∫ (x : E), (f (x + t • v) - f x) * g x ∂μ = ∫ (x : E), f x * (g (x + t • -v) - g x) ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<VAR>A : Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))<VAR>B : Tendsto (fun t => ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))<VAR>t : ℝ<VAR>S3 : ∫ (x : E), f (x + t • v) * g x ∂μ = ∫ (x : E), f x * g (x + t • -v) ∂μ<GOAL>∫ (x : E), (f (x + t • v) - f x) * g x ∂μ = ∫ (x : E), f x * (g (x + t • -v) - g x) ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<VAR>A : Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))<VAR>B : Tendsto (fun t => ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))<VAR>t : ℝ<VAR>S3 : ∫ (x : E), f (x + t • v) * g x ∂μ = ∫ (x : E), f x * g (x + t • -v) ∂μ<GOAL>∫ (x : E), f (x + t • v) * g x - f x * g x ∂μ = ∫ (x : E), f x * g (x + t • -v) - f x * g x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<VAR>A : Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))<VAR>B : Tendsto (fun t => ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))<VAR>t : ℝ<VAR>S3 : ∫ (x : E), f (x + t • v) * g x ∂μ = ∫ (x : E), f x * g (x + t • -v) ∂μ<GOAL>Integrable (fun x => f x * g (x + t • -v)) μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<VAR>A : Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))<VAR>B : Tendsto (fun t => ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))<VAR>t : ℝ<VAR>S3 : ∫ (x : E), f (x + t • v) * g x ∂μ = ∫ (x : E), f x * g (x + t • -v) ∂μ<GOAL>Integrable (fun x => f x * g x) μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : LipschitzWith D g<VAR>h'g : HasCompactSupport g<VAR>v : E<VAR>A : Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))<VAR>B : Tendsto (fun t => ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))<VAR>t : ℝ<VAR>S3 : ∫ (x : E), f (x + t • v) * g x ∂μ = ∫ (x : E), f x * g (x + t • -v) ∂μ<GOAL>Integrable (fun x => f (x + t • v) * g x) μ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>x✝ : M<VAR>f✝ : Dual R M<VAR>y : M<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : Φ.Finite<VAR>hx' : x ∈ span R Φ<VAR>f g : Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ<GOAL>(span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>x✝ : M<VAR>f✝ : Dual R M<VAR>y : M<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : Φ.Finite<VAR>hx' : x ∈ span R Φ<VAR>f g : Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ<VAR>Φ' : Set ↥(span R Φ) := range (inclusion ⋯)<GOAL>(span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>x✝ : M<VAR>f✝ : Dual R M<VAR>y : M<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : _root_.Finite ↑Φ<VAR>hx' : x ∈ span R Φ<VAR>f g : Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ<VAR>Φ' : Set ↥(span R Φ) := range (inclusion ⋯)<GOAL>(span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>x✝ : M<VAR>f✝ : Dual R M<VAR>y : M<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : _root_.Finite ↑Φ<VAR>hx' : x ∈ span R Φ<VAR>f g : Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ<VAR>Φ' : Set ↥(span R Φ) := range (inclusion ⋯)<VAR>hΦ'₁ : Φ'.Finite<GOAL>(span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>x✝ : M<VAR>f✝ : Dual R M<VAR>y : M<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : _root_.Finite ↑Φ<VAR>hx' : x ∈ span R Φ<VAR>f g : Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ<VAR>Φ' : Set ↥(span R Φ) := range (inclusion ⋯)<VAR>hΦ'₁ : Φ'.Finite<VAR>hΦ'₂ : span R Φ' = ⊤<VAR>x' : ↥(span R Φ) := ⟨x, hx'⟩<GOAL>(span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>x✝ : M<VAR>f✝ : Dual R M<VAR>y : M<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : _root_.Finite ↑Φ<VAR>hx'✝ : x ∈ span R Φ<VAR>f g : Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ<VAR>Φ' : Set ↥(span R Φ) := range (inclusion ⋯)<VAR>hΦ'₁ : Φ'.Finite<VAR>hΦ'₂ : span R Φ' = ⊤<VAR>x' : ↥(span R Φ) := ⟨x, hx'✝⟩<VAR>hx' : x' ≠ 0<GOAL>(span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>x✝ : M<VAR>f✝ : Dual R M<VAR>y : M<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : _root_.Finite ↑Φ<VAR>hx'✝ : x ∈ span R Φ<VAR>f g : Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ<VAR>Φ' : Set ↥(span R Φ) := range (inclusion ⋯)<VAR>hΦ'₁ : Φ'.Finite<VAR>hΦ'₂ : span R Φ' = ⊤<VAR>x' : ↥(span R Φ) := ⟨x, hx'✝⟩<VAR>hx' : x' ≠ 0<VAR>this : ∀ {F : Dual R M}, MapsTo (⇑(preReflection x F)) Φ Φ → MapsTo (⇑(preReflection x' ((span R Φ).subtype.dualMap F))) Φ' Φ'<GOAL>(span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : SemilatticeSup α<VAR>a : α<GOAL>Unbounded (fun x x_1 => x ≤ x_1) (s ∩ {b | ¬b ≤ a}) ↔ Unbounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : SemilatticeSup α<VAR>a : α<GOAL>Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | ¬b ≤ a}) ↔ Bounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Field β<VAR>inst✝ : ContinuousMul β<VAR>c : β<VAR>hc0 : c ≠ 0<VAR>h : SuperpolynomialDecay l k fun n => c * f n<VAR>x : α<GOAL>c⁻¹ * (c * f x) = f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<GOAL>(setToL1 hT) (indicatorConstLp 1 hs hμs x) = (T s) x