ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : SecondCountableTopology V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>μ : Measure V<VAR>n : ℕ<VAR>hf : Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ<VAR>h'f : AEStronglyMeasurable f μ<GOAL>Integrable (fun v => fourierPowSMulRight L f v n) μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : SecondCountableTopology V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>μ : Measure V<VAR>n : ℕ<VAR>hf : Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ<VAR>h'f : AEStronglyMeasurable f μ<GOAL>∀ᵐ (a : V) ∂μ, ‖fourierPowSMulRight L f a n‖ ≤ (2 * π * ‖L‖) ^ n * (‖a‖ ^ n * ‖f a‖)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : SecondCountableTopology V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>μ : Measure V<VAR>n : ℕ<VAR>hf : Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ<VAR>h'f : AEStronglyMeasurable f μ<VAR>v : V<GOAL>‖fourierPowSMulRight L f v n‖ ≤ (2 * π * ‖L‖) ^ n * (‖v‖ ^ n * ‖f v‖)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f'✝ : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>y : M<VAR>hy : y ∈ f.source<VAR>hgy : g y ∈ f'.source<VAR>hmaps : MapsTo g s f'.source<GOAL>Tendsto (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) y) (𝓝 ((↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I) y))) ↔ Tendsto g (𝓝[s] y) (𝓝 (g y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f'✝ : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>y : M<VAR>hy : y ∈ f.source<VAR>hgy : g y ∈ f'.source<VAR>hmaps : MapsTo g s f'.source<GOAL>Tendsto (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) y) (𝓝 (↑(f'.extend I') (g (↑(f.extend I).symm (↑(f.extend I) y))))) ↔ Tendsto g (𝓝[s] y) (𝓝 (g y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f'✝ : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>y : M<VAR>hy : y ∈ f.source<VAR>hgy : g y ∈ f'.source<VAR>hmaps : MapsTo g s f'.source<GOAL>∀ᶠ (z : E) in 𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) y, (g ∘ ↑(f.extend I).symm) z ∈ f'.source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f'✝ : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>y : M<VAR>hy : y ∈ f.source<VAR>hgy : g y ∈ f'.source<VAR>hmaps : MapsTo g s f'.source<GOAL>∀ᶠ (a : M) in 𝓝[s] y, (g ∘ ↑(f.extend I).symm) (↑(f.extend I) a) ∈ f'.source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f'✝ : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>y : M<VAR>hy : y ∈ f.source<VAR>hgy : g y ∈ f'.source<VAR>hmaps : MapsTo g s f'.source<VAR>z : M<VAR>hz : z ∈ s ∩ f.source<GOAL>(g ∘ ↑(f.extend I).symm) (↑(f.extend I) z) ∈ f'.source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f'✝ : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>y : M<VAR>hy : y ∈ f.source<VAR>hgy : g y ∈ f'.source<VAR>hmaps : MapsTo g s f'.source<VAR>z : M<VAR>hz : z ∈ s ∩ f.source<GOAL>g z ∈ f'.source
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>(dualPairing 𝕜 E).SeparatingLeft
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>Function.Injective ⇑(dualPairing 𝕜 E)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Module A M<VAR>inst✝⁵ : Module B M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : IsScalarTower R A M<VAR>inst✝¹ : IsScalarTower R B M<VAR>inst✝ : SMulCommClass A B M<VAR>p : Submodule (A ⊗[R] B) M<VAR>a : A<VAR>m : M<VAR>hm : m ∈ p<GOAL>a • m ∈ p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Module A M<VAR>inst✝⁵ : Module B M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : IsScalarTower R A M<VAR>inst✝¹ : IsScalarTower R B M<VAR>inst✝ : SMulCommClass A B M<VAR>p : Submodule (A ⊗[R] B) M<VAR>a : A<VAR>m : M<VAR>hm : m ∈ p<GOAL>a • m = a ⊗ₜ[R] 1 • m
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>M : Matrix m m' R<GOAL>(toMatrix₂' R) B * M = (toMatrix₂' R) (B.compl₂ (toLin' M))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>{a}.max = ↑a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>(insert a ∅).max = ↑a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>s : Finset ι<VAR>hv : Orthonormal 𝕜 v<GOAL>∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2 ≤ ‖x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>s : Finset ι<VAR>hv : Orthonormal 𝕜 v<VAR>h₂ : ∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫_𝕜 * ⟪x, v j⟫_𝕜 * ⟪v j, v i⟫_𝕜 = ∑ k ∈ s, ⟪v k, x⟫_𝕜 * ⟪x, v k⟫_𝕜<GOAL>∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2 ≤ ‖x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>s : Finset ι<VAR>hv : Orthonormal 𝕜 v<VAR>h₂ : ∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫_𝕜 * ⟪x, v j⟫_𝕜 * ⟪v j, v i⟫_𝕜 = ∑ k ∈ s, ⟪v k, x⟫_𝕜 * ⟪x, v k⟫_𝕜<VAR>h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2<GOAL>∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2 ≤ ‖x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>s : Finset ι<VAR>hv : Orthonormal 𝕜 v<VAR>h₂ : ∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫_𝕜 * ⟪x, v j⟫_𝕜 * ⟪v j, v i⟫_𝕜 = ∑ k ∈ s, ⟪v k, x⟫_𝕜 * ⟪x, v k⟫_𝕜<VAR>h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2<GOAL>‖x - ∑ i ∈ s, ⟪v i, x⟫_𝕜 • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>s : Finset ι<VAR>hv : Orthonormal 𝕜 v<VAR>h₂ : ∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫_𝕜 * ⟪x, v j⟫_𝕜 * ⟪v j, v i⟫_𝕜 = ∑ k ∈ s, ⟪v k, x⟫_𝕜 * ⟪x, v k⟫_𝕜<VAR>h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2<GOAL>‖x‖ ^ 2 - (2 * re ⟪x, ∑ i ∈ s, ⟪v i, x⟫_𝕜 • v i⟫_𝕜 - ‖∑ i ∈ s, ⟪v i, x⟫_𝕜 • v i‖ ^ 2) = ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>s : Finset ι<VAR>hv : Orthonormal 𝕜 v<VAR>h₂ : ∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫_𝕜 * ⟪x, v j⟫_𝕜 * ⟪v j, v i⟫_𝕜 = ∑ k ∈ s, ⟪v k, x⟫_𝕜 * ⟪x, v k⟫_𝕜<VAR>h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2<GOAL>re ⟪x, x⟫_𝕜 - (2 * re (∑ i ∈ s, ⟪x, ⟪v i, x⟫_𝕜 • v i⟫_𝕜) - re (∑ x_1 ∈ s, ∑ i ∈ s, ⟪⟪v i, x⟫_𝕜 • v i, ⟪v x_1, x⟫_𝕜 • v x_1⟫_𝕜)) = re ⟪x, x⟫_𝕜 - ∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>s : Finset ι<VAR>hv : Orthonormal 𝕜 v<VAR>h₂ : ∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫_𝕜 * ⟪x, v j⟫_𝕜 * ⟪v j, v i⟫_𝕜 = ∑ k ∈ s, ⟪v k, x⟫_𝕜 * ⟪x, v k⟫_𝕜<VAR>h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2<GOAL>re (∑ x_1 ∈ s, ⟪v x_1, x⟫_𝕜 * ⟪x, v x_1⟫_𝕜) = ∑ i ∈ s, ‖⟪v i, x⟫_𝕜‖ ^ 2
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>β' : Weight K (↥H) L<VAR>n : ℤ<VAR>hβ' : ⇑β' = n • ⇑α + ⇑β<GOAL>↑(chainTopCoeff (⇑α) β') = ↑(chainTopCoeff (⇑α) β) - n
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>β' : Weight K (↥H) L<VAR>n : ℤ<VAR>hβ' : ⇑β' = n • ⇑α + ⇑β<GOAL>↑(chainTopCoeff (⇑α) β') ≤ ↑(chainTopCoeff (⇑α) β) - n
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>β' : Weight K (↥H) L<VAR>n : ℤ<VAR>hβ' : ⇑β' = n • ⇑α + ⇑β<GOAL>↑(chainTopCoeff (⇑α) β) - n ≤ ↑(chainTopCoeff (⇑α) β')
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₁.RightHomologyData<VAR>h₁' : S₂.LeftHomologyData<VAR>h₂' : S₂.RightHomologyData<GOAL>leftHomologyMap' φ h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' = leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' φ h₂ h₂'
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i✝ : Fact (finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>_i : Fact (finrank ℝ E = 0)<GOAL>positiveOrientation.volumeForm = AlternatingMap.constLinearEquivOfIsEmpty 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<GOAL>UniformEquicontinuous F ↔ UniformContinuous (⇑UniformFun.ofFun ∘ swap F)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<GOAL>UniformEquicontinuous F ↔ ∀ i ∈ 𝓤 α, ∀ᶠ (x : β × β) in 𝓤 β, ((⇑UniformFun.ofFun ∘ swap F) x.1, (⇑UniformFun.ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α i
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>a : α<VAR>P : Finpartition a<VAR>b : α<VAR>hb : b ∈ P.parts<VAR>h : b = ⊥<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>a : α<VAR>P : Finpartition a<VAR>b : α<VAR>hb : b ∈ P.parts<VAR>h : b = ⊥<GOAL>⊥ ∈ P.parts
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : ι → α<VAR>htriv : ¬∀ (i : ι), f i = ⊥<GOAL>⨆ i, f ↑i = ⨆ i, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : ι → α<VAR>htriv : ¬∀ (i : ι), f i = ⊥<VAR>i : ι<GOAL>∃ i', f i ≤ f ↑i'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CommSemiring α<VAR>s✝ : Multiset (Multiset α)<VAR>a : Multiset α<VAR>s : Multiset (Multiset α)<VAR>ih : (map sum s).prod = (map prod s.Sections).sum<GOAL>(map sum (a ::ₘ s)).prod = (map prod (a ::ₘ s).Sections).sum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<VAR>hf : Monotone f<VAR>n : ℕ<GOAL>disjointed f (n + 1) ⊔ f n = f (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<VAR>hf : Monotone f<VAR>n : ℕ<GOAL>f n ≤ f (n + 1)
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ r₁ r₂ : List α<VAR>e' : l₂.append r₂ = l₁.append r₁<VAR>ll : (a :: l₁).length ≤ (a :: l₂).length<GOAL>a :: l₁ <+: a :: l₂
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ r₁ r₂ r₃ : List α<VAR>e' : (l₁ ++ r₃).append r₂ = l₁.append r₁<VAR>ll : (a :: l₁).length ≤ (a :: (l₁ ++ r₃)).length<GOAL>a :: l₁ <+: a :: (l₁ ++ r₃)
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedHurwitzZetaOdd (-a) s = -completedHurwitzZetaOdd a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>(∫ (t : ℝ) in Ioi 0, -(↑t ^ ((s + 1) / 2 - 1) • ↑(oddKernel a t))) / 2 = -((∫ (t : ℝ) in Ioi 0, ↑t ^ ((s + 1) / 2 - 1) • ↑(oddKernel a t)) / 2)
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>max (aleph o₁) (aleph o₂) = aleph (max o₁ o₂)
<VAR>o₁ o₂ : Ordinal.{u_1}<VAR>h : aleph o₁ ≤ aleph o₂<GOAL>max (aleph o₁) (aleph o₂) = aleph (max o₁ o₂)
<VAR>o₁ o₂ : Ordinal.{u_1}<VAR>h : aleph o₂ ≤ aleph o₁<GOAL>max (aleph o₁) (aleph o₂) = aleph (max o₁ o₂)
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>n : ℤ<VAR>y : ℝ := rexp (-π * τ.im)<GOAL>‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>n : ℤ<VAR>y : ℝ := rexp (-π * τ.im)<VAR>h : y < 1<GOAL>‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>n : ℤ<VAR>y : ℝ := rexp (-π * τ.im)<VAR>h : y < 1<GOAL>‖cexp (↑π * I * ↑n ^ 2 * τ)‖ = y ^ n ^ 2
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>n : ℤ<VAR>y : ℝ := rexp (-π * τ.im)<VAR>h : y < 1<GOAL>y ^ n ^ 2 ≤ rexp (-π * τ.im) ^ n.natAbs
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>u v : E<GOAL>v ∈ (span 𝕜 {u})ᗮ ↔ ⟪u, v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>u v : E<GOAL>⟪u, v⟫_𝕜 = 0 → v ∈ (span 𝕜 {u})ᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>u v : E<VAR>hv : ⟪u, v⟫_𝕜 = 0<VAR>w : E<VAR>hw : w ∈ span 𝕜 {u}<GOAL>⟪w, v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>u v : E<VAR>hv : ⟪u, v⟫_𝕜 = 0<VAR>w : E<VAR>hw : ∃ a, a • u = w<GOAL>⟪w, v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>u v : E<VAR>hv : ⟪u, v⟫_𝕜 = 0<VAR>c : 𝕜<GOAL>⟪c • u, v⟫_𝕜 = 0
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>r : R<VAR>n : ℕ<VAR>inst✝ : n.AtLeastTwo<GOAL>r * OfNat.ofNat n = n • r
<VAR>ι : Type u_1<VAR>ι'✝ : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b : Basis ι R M<VAR>b'✝ : Basis ι'✝ R M'<VAR>ι' : Type u_10<VAR>inst✝ : Fintype ι'<VAR>b' : Basis ι' R M<VAR>x : M<VAR>i : ι<GOAL>∑ j : ι', (b.repr (b' j)) i * (b'.repr x) j = (b.repr x) i
<VAR>ι : Type u_1<VAR>ι'✝ : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b : Basis ι R M<VAR>b'✝ : Basis ι'✝ R M'<VAR>ι' : Type u_10<VAR>inst✝ : Fintype ι'<VAR>b' : Basis ι' R M<VAR>x : M<VAR>i : ι<GOAL>∑ j : ι', (b.repr (b' j)) i * (b'.repr x) j = (b.repr (∑ i : ι', (b'.repr x) i • b' i)) i
<VAR>ι : Type u_1<VAR>ι'✝ : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b : Basis ι R M<VAR>b'✝ : Basis ι'✝ R M'<VAR>ι' : Type u_10<VAR>inst✝ : Fintype ι'<VAR>b' : Basis ι' R M<VAR>x : M<VAR>i : ι<GOAL>∑ j : ι', (b.repr (b' j)) i * (b'.repr x) j = ∑ k : ι', ((b'.repr x) k • b.repr (b' k)) i
<VAR>ι : Type u_1<VAR>ι'✝ : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b : Basis ι R M<VAR>b'✝ : Basis ι'✝ R M'<VAR>ι' : Type u_10<VAR>inst✝ : Fintype ι'<VAR>b' : Basis ι' R M<VAR>x : M<VAR>i : ι<VAR>j : ι'<VAR>x✝ : j ∈ Finset.univ<GOAL>(b.repr (b' j)) i * (b'.repr x) j = ((b'.repr x) j • b.repr (b' j)) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (s ×ˢ t) (κ a)<GOAL>∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ t, f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (s ×ˢ t) (κ a)<GOAL>∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (s ×ˢ t) ((κ.fst ⊗ₖ κ.condKernel) a)<GOAL>∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel) a