ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : Preorder γ<VAR>inst✝ : Preorder δ<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : StrictAnti f<VAR>hg : StrictAnti g<VAR>a b : α × β<GOAL>a < b → Prod.map f g b < Prod.map f g a
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : Preorder γ<VAR>inst✝ : Preorder δ<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : StrictAnti f<VAR>hg : StrictAnti g<VAR>a b : α × β<GOAL>a.1 < b.1 ∧ a.2 ≤ b.2 ∨ a.1 ≤ b.1 ∧ a.2 < b.2 → (Prod.map f g b).1 < (Prod.map f g a).1 ∧ (Prod.map f g b).2 ≤ (Prod.map f g a).2 ∨ (Prod.map f g b).1 ≤ (Prod.map f g a).1 ∧ (Prod.map f g b).2 < (Prod.map f g a).2
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>κ : Type u_1<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>inst✝¹ : (i : ι) → DecidableEq (α i)<VAR>inst✝ : (i : ι) → (j : α i) → Zero (δ i j)<VAR>i : ι<VAR>j : α i<VAR>x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd<VAR>i' : ι<VAR>j' : α i'<GOAL>((single ⟨i, j⟩ x).sigmaCurry i') j' = ((single i (single j x)) i') j'
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>κ : Type u_1<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>inst✝¹ : (i : ι) → DecidableEq (α i)<VAR>inst✝ : (i : ι) → (j : α i) → Zero (δ i j)<VAR>i : ι<VAR>j : α i<VAR>x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd<VAR>i' : ι<VAR>j' : α i'<GOAL>(single ⟨i, j⟩ x) ⟨i', j'⟩ = ((single i (single j x)) i') j'
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>κ : Type u_1<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>inst✝¹ : (i : ι) → DecidableEq (α i)<VAR>inst✝ : (i : ι) → (j : α i) → Zero (δ i j)<VAR>i : ι<VAR>j : α i<VAR>x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd<VAR>j' : α i<GOAL>(single ⟨i, j⟩ x) ⟨i, j'⟩ = ((single i (single j x)) i) j'
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>κ : Type u_1<VAR>α : ι → Type u_2<VAR>δ : (i : ι) → α i → Type v<VAR>inst✝¹ : (i : ι) → DecidableEq (α i)<VAR>inst✝ : (i : ι) → (j : α i) → Zero (δ i j)<VAR>i : ι<VAR>j : α i<VAR>x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd<VAR>i' : ι<VAR>j' : α i'<VAR>hi : i ≠ i'<GOAL>(single ⟨i, j⟩ x) ⟨i', j'⟩ = ((single i (single j x)) i') j'
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))<VAR>a✝ : x ∈ ⊤<GOAL>x ∈ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))<VAR>a✝ : x ∈ ⊤<GOAL>∃ c, ∑ i : G.ConnectedComponent, c i • G.lapMatrix_ker_basis_aux i = x
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))<VAR>a✝ : x ∈ ⊤<GOAL>∑ i : G.ConnectedComponent, Quot.lift ↑x ⋯ i • G.lapMatrix_ker_basis_aux i = x
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))<VAR>a✝ : x ∈ ⊤<VAR>j : V<GOAL>↑(∑ i : G.ConnectedComponent, Quot.lift ↑x ⋯ i • G.lapMatrix_ker_basis_aux i) j = ↑x j
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>x : ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))<VAR>a✝ : x ∈ ⊤<VAR>j : V<GOAL>Quot.lift ↑x ⋯ (G.connectedComponentMk j) = ↑x j
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : CommRing A<VAR>inst✝ : CommRing B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hmap : map f p ≠ 0<VAR>a : A<GOAL>rootMultiplicity a p ≤ rootMultiplicity (f a) (map f p)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : CommRing A<VAR>inst✝ : CommRing B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hmap : map f p ≠ 0<VAR>a : A<GOAL>(X - C (f a)) ^ rootMultiplicity a p ∣ map f p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : CommRing A<VAR>inst✝ : CommRing B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hmap : map f p ≠ 0<VAR>a : A<GOAL>(X - C (f a)) ^ rootMultiplicity a p ∣ (mapRingHom f) ((X - C a) ^ rootMultiplicity a p)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>x : ↥H<VAR>α : ↥H → K<VAR>hαx : α x = 0<VAR>hx : x ∈ corootSpace α<GOAL>x = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>x : ↥H<VAR>hαx : 0 x = 0<VAR>hx : x ∈ corootSpace 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>x : ↥H<VAR>α : ↥H → K<VAR>hαx : α x = 0<VAR>hx : x ∈ corootSpace α<VAR>hα : α ≠ 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>x : ↥H<VAR>α : ↥H → K<VAR>hαx : α x = 0<VAR>hα : α ≠ 0<VAR>hx : x ∈ ⨅ β, Weight.ker<GOAL>x = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f g : α → E<VAR>hfg : f =ᶠ[ae μ] g<GOAL>Memℒp f p μ ↔ Memℒp g p μ
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>x : ℝ<VAR>hx : rexp 1 ≤ x<GOAL>1 + ε x ≤ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>x : ℝ<VAR>hx : rexp 1 ≤ x<GOAL>1 + 1 / log x ≤ 1 + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>x : ℝ<VAR>hx : rexp 1 ≤ x<VAR>this : 1 < x<GOAL>1 / log x ≤ 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>x : ℝ<VAR>hx : rexp 1 ≤ x<VAR>this : 1 < x<GOAL>1 ≤ log x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<GOAL>f.IsCycle ↔ ∃ s, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hf : f.IsCycle<GOAL>{x | f x ≠ x}.Nontrivial
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<GOAL>(∃ s, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s) → f.IsCycle
<VAR>p : ℕ<VAR>hp : 1 < p<VAR>inst✝ : Fintype (ZMod p)ˣ<GOAL>Fintype.card (ZMod p)ˣ ≤ p - 1
<VAR>p : ℕ<VAR>hp : 1 < p<VAR>inst✝ : Fintype (ZMod p)ˣ<VAR>this : NeZero p<GOAL>Fintype.card (ZMod p)ˣ ≤ p - 1
<VAR>p : ℕ<VAR>hp : 1 < p<VAR>inst✝ : Fintype (ZMod p)ˣ<VAR>this : NeZero p<GOAL>φ p ≤ p - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>x : γ<VAR>s s' : Set β<VAR>h : s ⊆ s'<GOAL>κ.density ν a x s ≤ κ.density ν a x s'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>x : γ<VAR>s s' : Set β<VAR>h : s ⊆ s'<GOAL>(fun n => κ.densityProcess ν n a x s) ≤ᶠ[atTop] fun n => κ.densityProcess ν n a x s'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>x : γ<VAR>s s' : Set β<VAR>h : s ⊆ s'<GOAL>IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop fun n => κ.densityProcess ν n a x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>x : γ<VAR>s s' : Set β<VAR>h : s ⊆ s'<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun n => κ.densityProcess ν n a x s'
<VAR>α : Type u_1<VAR>n m : ℕ<VAR>H : Raised n m<GOAL>m.dist n ≤ 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>‖indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>V : Type u_5<VAR>W : Type u_6<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedAddCommGroup V<VAR>inst✝¹² : NormedSpace 𝕜 V<VAR>inst✝¹¹ : MeasurableSpace V<VAR>inst✝¹⁰ : BorelSpace V<VAR>inst✝⁹ : NormedAddCommGroup W<VAR>inst✝⁸ : NormedSpace 𝕜 W<VAR>inst✝⁷ : MeasurableSpace W<VAR>inst✝⁶ : BorelSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →L[𝕜] W →L[𝕜] 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>M : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝ : (i : ι) → NormedSpace ℝ (M i)<VAR>f : V → ContinuousMultilinearMap ℝ M E<VAR>m : (i : ι) → M i<VAR>w : W<VAR>he : Continuous ⇑e<VAR>hf : Integrable f μ<GOAL>(fourierIntegral e μ L.toLinearMap₂ f w) m = fourierIntegral e μ L.toLinearMap₂ (fun x => (f x) m) w
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>V : Type u_5<VAR>W : Type u_6<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedAddCommGroup V<VAR>inst✝¹² : NormedSpace 𝕜 V<VAR>inst✝¹¹ : MeasurableSpace V<VAR>inst✝¹⁰ : BorelSpace V<VAR>inst✝⁹ : NormedAddCommGroup W<VAR>inst✝⁸ : NormedSpace 𝕜 W<VAR>inst✝⁷ : MeasurableSpace W<VAR>inst✝⁶ : BorelSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →L[𝕜] W →L[𝕜] 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>M : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝ : (i : ι) → NormedSpace ℝ (M i)<VAR>f : V → ContinuousMultilinearMap ℝ M E<VAR>m : (i : ι) → M i<VAR>w : W<VAR>he : Continuous ⇑e<VAR>hf : Integrable f μ<GOAL>∫ (x : V), (e (-(L.toLinearMap₂ x) w) • f x) m ∂μ = fourierIntegral e μ L.toLinearMap₂ (fun x => (f x) m) w
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>V : Type u_5<VAR>W : Type u_6<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedAddCommGroup V<VAR>inst✝¹² : NormedSpace 𝕜 V<VAR>inst✝¹¹ : MeasurableSpace V<VAR>inst✝¹⁰ : BorelSpace V<VAR>inst✝⁹ : NormedAddCommGroup W<VAR>inst✝⁸ : NormedSpace 𝕜 W<VAR>inst✝⁷ : MeasurableSpace W<VAR>inst✝⁶ : BorelSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →L[𝕜] W →L[𝕜] 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>M : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝ : (i : ι) → NormedSpace ℝ (M i)<VAR>f : V → ContinuousMultilinearMap ℝ M E<VAR>m : (i : ι) → M i<VAR>w : W<VAR>he : Continuous ⇑e<VAR>hf : Integrable f μ<GOAL>Integrable (fun v => e (-(L.toLinearMap₂ v) w) • f v) μ
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>aux : ↑|0| ^ s = 0<GOAL>HasSum (fun n => if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>aux : ↑|0| ^ s = 0<VAR>hint : HasSum (fun n => s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 + s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2) (completedCosZeta (↑a) s + s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)<GOAL>HasSum (fun n => if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>aux : ↑|0| ^ s = 0<VAR>hint : HasSum (fun n => s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 + s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2) (completedCosZeta (↑a) s)<GOAL>HasSum (fun n => if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>aux : ↑|0| ^ s = 0<VAR>hint : HasSum (fun n => s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 + s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2) (completedCosZeta (↑a) s)<VAR>n : ℕ<GOAL>(if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) = s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 + s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<GOAL>Group.IsNilpotent G ↔ ∃ n, lowerCentralSeries G n = ⊥
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<GOAL>(∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) ↔ ∃ n, lowerCentralSeries G n = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>x : M<VAR>hx : x ∈ I • N<VAR>p : (x : M) → x ∈ I • N → Prop<VAR>smul : ∀ (r : R) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯<VAR>add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯<GOAL>p x hx
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>x : M<VAR>hx : x ∈ I • N<VAR>p : (x : M) → x ∈ I • N → Prop<VAR>smul : ∀ (r : R) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯<VAR>add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯<GOAL>∃ (x_1 : x ∈ I • N), p x x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>c : E''<VAR>hc : c ≠ 0<GOAL>(fun _x => c) =o[l] g ↔ Tendsto (fun x => ‖g x‖) l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>c : E''<VAR>hc : c ≠ 0<GOAL>(fun _x => c) =o[l] g ↔ (fun _x => 1) =o[l] g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>L : List (List α)<VAR>i : ℕ<GOAL>drop (take i (map length L)).sum L.join = (drop i L).join
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsInitSeg 𝒜 r<VAR>h𝒜₀ : 𝒜.Nonempty<GOAL>∃ s, s.card = r ∧ 𝒜 = initSeg s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsInitSeg 𝒜 r<VAR>h𝒜₀ : 𝒜.Nonempty<VAR>hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜<GOAL>∃ s, s.card = r ∧ 𝒜 = initSeg s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsInitSeg 𝒜 r<VAR>h𝒜₀ : 𝒜.Nonempty<VAR>hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜<GOAL>𝒜 = initSeg (𝒜.sup' h𝒜₀ toColex).ofColex
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t✝ u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsInitSeg 𝒜 r<VAR>h𝒜₀ : 𝒜.Nonempty<VAR>hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜<VAR>t : Finset α<GOAL>t ∈ 𝒜 ↔ t ∈ initSeg (𝒜.sup' h𝒜₀ toColex).ofColex
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t✝ u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsInitSeg 𝒜 r<VAR>h𝒜₀ : 𝒜.Nonempty<VAR>hs : 𝒜.sup' h𝒜₀ toColex ∈ ofColex ⁻¹' ↑𝒜<VAR>t : Finset α<GOAL>t ∈ 𝒜 ↔ (𝒜.sup' h𝒜₀ toColex).ofColex.card = t.card ∧ { ofColex := t } ≤ { ofColex := (𝒜.sup' h𝒜₀ toColex).ofColex }
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>-(Complex.I * (Complex.I * (o.kahler x) y)) = (o.kahler x) y
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ≥0<VAR>hfm : AEStronglyMeasurable f μ<VAR>hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ↑I<GOAL>∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal ↑I
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ<VAR>hc : c < 1<GOAL>∀ᶠ (x : ℝ) in atTop, c < 1 - ε x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ<VAR>hc : c < 1<VAR>h₁ : Tendsto (fun x => 1 - ε x) atTop (𝓝 1)<GOAL>∀ᶠ (x : ℝ) in atTop, c < 1 - ε x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ<VAR>hc : c < 1<VAR>h₁ : (∀ a' < 1, ∀ᶠ (b : ℝ) in atTop, a' < 1 - ε b) ∧ ∀ a' > 1, ∀ᶠ (b : ℝ) in atTop, 1 - ε b < a'<GOAL>∀ᶠ (x : ℝ) in atTop, c < 1 - ε x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler x) y = (starRingEnd ℂ) ((o.kahler y) x)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>↑⟪x, y⟫_ℝ + (o.areaForm x) y • Complex.I = (starRingEnd ℂ) (↑⟪y, x⟫_ℝ + (o.areaForm y) x • Complex.I)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>↑⟪y, x⟫_ℝ + -(o.areaForm y) x • Complex.I = (starRingEnd ℂ) (↑⟪y, x⟫_ℝ + (o.areaForm y) x • Complex.I)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<VAR>h : IsUnit z<GOAL>‖z‖ = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<VAR>h : IsUnit z<VAR>w : ℤ_[p]<VAR>eq : 1 = z * w<GOAL>‖z‖ = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<VAR>h : IsUnit z<VAR>w : ℤ_[p]<VAR>eq : 1 = z * w<GOAL>1 ≤ ‖z‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<VAR>h : IsUnit z<VAR>w : ℤ_[p]<VAR>eq : 1 = z * w<VAR>this : ‖z‖ * ‖w‖ ≤ ‖z‖ * 1<GOAL>1 ≤ ‖z‖
<VAR>a x z : ℂ<VAR>θ : ℝ<VAR>hθ : θ ∈ Ioc (-π) π<GOAL>(cos ↑θ + sin ↑θ * I).arg = θ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t✝ u : Finset α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>t : Finset β<VAR>f : ℕ → α<VAR>hf : ∀ i < n, f i ∈ s<VAR>f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j<GOAL>∀ a ∈ range n, f a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<GOAL>∀ᵐ (x : α) ∂μ, 0 < μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<GOAL>∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0 → 0 < μ.rnDeriv ν x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀✝ w : ℂ<VAR>ε r m : ℝ<VAR>z₀ : E<VAR>hg : AnalyticAt ℂ g z₀<VAR>ray : E → ℂ → E := fun z t => z₀ + t • z<VAR>gray : E → ℂ → ℂ := fun z => g ∘ ray z<GOAL>(∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)