ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<GOAL>∃ B, (fun x => invInterpStrip f x ε • f x) =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z => Real.exp (B * Real.exp (0 * |z.im|))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>BF : ℝ<VAR>hBF : BF ∈ upperBounds (norm ∘ F f ε '' verticalClosedStrip 0 1)<GOAL>∃ B, (fun x => invInterpStrip f x ε • f x) =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z => Real.exp (B * Real.exp (0 * |z.im|))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>BF : ℝ<VAR>hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF<GOAL>∃ B, (fun x => invInterpStrip f x ε • f x) =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z => Real.exp (B * Real.exp (0 * |z.im|))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>BF : ℝ<VAR>hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF<GOAL>(fun x => invInterpStrip f x ε • f x) =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z => Real.exp (BF * Real.exp (0 * |z.im|))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>BF : ℝ<VAR>hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF<GOAL>∃ c, ∀ᶠ (x : ℂ) in comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1), ‖invInterpStrip f x ε • f x‖ ≤ c * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>BF : ℝ<VAR>hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF<GOAL>∀ᶠ (x : ℂ) in comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1), ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>BF : ℝ<VAR>hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF<GOAL>∀ᶠ (x : ℂ) in comap (_root_.abs ∘ im) atTop, x ∈ re ⁻¹' Ioo 0 1 → ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>BF : ℝ<VAR>hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF<GOAL>∀ x ∈ re ⁻¹' Ioo 0 1, ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>BF : ℝ<VAR>hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF<VAR>x : ℂ<VAR>hx : x ∈ re ⁻¹' Ioo 0 1<GOAL>‖invInterpStrip f x ε • f x‖ ≤ Real.exp BF
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>hb : b ≠ 0<VAR>h : a * c⁻¹ = b<GOAL>a = b * c
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>hb : b ≠ 0<VAR>h : a * c⁻¹ = b<GOAL>c ≠ 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b d : G₀<VAR>m n : ℕ<VAR>hb : b ≠ 0<VAR>h : a * 0⁻¹ = b<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>inst✝ : OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>l : Filter α<VAR>hf : IsMaxOn f s a<VAR>hg : IsMinOn g s a<GOAL>IsMaxOn (fun x => f x - g x) s a
<VAR>m k : ℕ<GOAL>hyperoperation 0 m k = k.succ
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Group M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>ha : Function.Surjective fun r => a • r<VAR>x✝ : R<GOAL>x✝ ∈ (a • S).toAddSubmonoid ↔ x✝ ∈ a • S.toAddSubmonoid
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>h : IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<VAR>f : α → E<VAR>hf : Integrable f ν<GOAL>∫ (x : α), f x ∂ν = ∑' (g : G), ∫ (x : α) in g • s, f x ∂ν
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>h : IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<VAR>f : α → E<VAR>hf : Integrable f ν<GOAL>Integrable f (sum fun g => ν.restrict (g • s))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : Group H<VAR>inst✝¹⁰ : MulAction G α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MulAction H β<VAR>inst✝⁷ : MeasurableSpace β<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>h : IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<VAR>f : α → E<VAR>hf : Integrable f ν<GOAL>Integrable f ν
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (E i)<VAR>s : (i : ι) → Set (Set (E i))<VAR>hs : ∀ (i : ι), IsTopologicalBasis (s i)<GOAL>IsTopologicalBasis (⋃ i, (fun u => Sigma.mk i '' u) '' s i)
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (E i)<VAR>s : (i : ι) → Set (Set (E i))<VAR>hs : ∀ (i : ι), IsTopologicalBasis (s i)<VAR>a : (i : ι) × E i<GOAL>(𝓝 a).HasBasis (fun t => t ∈ ⋃ i, (fun u => Sigma.mk i '' u) '' s i ∧ a ∈ t) id
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (E i)<VAR>s : (i : ι) → Set (Set (E i))<VAR>hs : ∀ (i : ι), IsTopologicalBasis (s i)<VAR>a : (i : ι) × E i<GOAL>(map (Sigma.mk a.fst) (𝓝 a.snd)).HasBasis (fun t => t ∈ ⋃ i, (fun u => Sigma.mk i '' u) '' s i ∧ a ∈ t) id
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (E i)<VAR>s : (i : ι) → Set (Set (E i))<VAR>hs : ∀ (i : ι), IsTopologicalBasis (s i)<VAR>a : (i : ι) × E i<VAR>x✝ : Set ((i : ι) × E i)<GOAL>x✝ ∈ ⋃ i, (fun u => Sigma.mk i '' u) '' s i ∧ a ∈ x✝ ↔ x✝ ∈ (fun i => Sigma.mk a.fst '' i) '' {i | i ∈ s a.fst ∧ a.snd ∈ i}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<GOAL>f.SameCycle x (f y) ↔ f.SameCycle x y
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin (n + 1) → ℤ<GOAL>↑(sf n) ∣ (Matrix.vandermonde v).det
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin (n + 1) → ℤ<VAR>m : ℤ := univ.inf' ⋯ v<GOAL>↑(sf n) ∣ (Matrix.vandermonde v).det
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin (n + 1) → ℤ<VAR>m : ℤ := univ.inf' ⋯ v<VAR>w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat<GOAL>↑(sf n) ∣ (Matrix.vandermonde v).det
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin (n + 1) → ℤ<VAR>m : ℤ := univ.inf' ⋯ v<VAR>w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat<VAR>hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m<GOAL>↑(sf n) ∣ (Matrix.vandermonde v).det
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin (n + 1) → ℤ<VAR>m : ℤ := univ.inf' ⋯ v<VAR>w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat<VAR>hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m<VAR>h : (Matrix.vandermonde fun i => ↑(w' i)).det = (Matrix.of fun i j => Polynomial.eval ((fun i => ↑(w' i)) i) ((fun i => descPochhammer ℤ ↑i) j)).det<GOAL>↑(sf n) ∣ (Matrix.vandermonde v).det
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin (n + 1) → ℤ<VAR>m : ℤ := univ.inf' ⋯ v<VAR>w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat<VAR>hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m<VAR>h : (Matrix.vandermonde v).det = (Matrix.of fun i j => Polynomial.eval ((fun i => ↑(w' i)) i) ((fun i => descPochhammer ℤ ↑i) j)).det<GOAL>↑(sf n) ∣ (Matrix.vandermonde v).det
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin (n + 1) → ℤ<VAR>m : ℤ := univ.inf' ⋯ v<VAR>w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat<VAR>hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m<VAR>h : (Matrix.vandermonde v).det = (Matrix.of fun i j => Polynomial.eval ((fun i => ↑(w' i)) i) ((fun i => descPochhammer ℤ ↑i) j)).det<GOAL>(Matrix.vandermonde v).det = ↑(sf n) * (Matrix.of fun i j => ↑((w' i).choose ↑j)).det
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ≤ a \ b ⊔ b
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>Integrable (fun x => x * rexp (-b * x ^ 2)) volume
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Countable ι<VAR>f : ι → Set α<VAR>hn : Pairwise (Disjoint on f)<VAR>h : ∀ (i : ι), MeasurableSet (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>m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Countable ι<VAR>f : ι → Set α<VAR>hn : Pairwise (Disjoint on f)<VAR>h : ∀ (i : ι), MeasurableSet (f i)<GOAL>∑' (i : ι), extend (fun t _ht => μ t) (f i) = ∑' (i : ι), μ (f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Countable ι<VAR>f : ι → Set α<VAR>hn : Pairwise (Disjoint on f)<VAR>h : ∀ (i : ι), MeasurableSet (f i)<GOAL>μ ∅ = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Countable ι<VAR>f : ι → Set α<VAR>hn : Pairwise (Disjoint on f)<VAR>h : ∀ (i : ι), MeasurableSet (f i)<GOAL>∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → μ (⋃ i, f i) = ∑' (i : ℕ), μ (f i)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω<VAR>hg : Submartingale g ℱ μ<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω<VAR>hg : Submartingale g ℱ μ<VAR>hg0 : g 0 = 0<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω<VAR>hg : Submartingale g ℱ μ<VAR>hg0 : g 0 = 0<VAR>hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω<VAR>hg : Submartingale g ℱ μ<VAR>hg0 : g 0 = 0<VAR>hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R<VAR>ω : Ω<VAR>hω : BddAbove (Set.range fun n => g n ω) ↔ ∃ c, Tendsto (fun n => g n ω) atTop (𝓝 c)<GOAL>BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>e : M ≃ₗ[R] N<GOAL>IsBaseChange R ↑e
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>e : M ≃ₗ[R] N<GOAL>∀ (Q : Type (max v₁ v₂ u_1)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module R Q] [inst_3 : IsScalarTower R R Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ ↑e = g
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q✝ : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q✝<VAR>inst✝ : Module S Q✝<VAR>e : M ≃ₗ[R] N<VAR>Q : Type (max v₁ v₂ u_1)<VAR>I₁ : AddCommMonoid Q<VAR>I₂ I₃ : Module R Q<VAR>I₄ : IsScalarTower R R Q<VAR>g : M →ₗ[R] Q<GOAL>∃! g', ↑R g' ∘ₗ ↑e = g
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q✝ : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q✝<VAR>inst✝ : Module S Q✝<VAR>e : M ≃ₗ[R] N<VAR>Q : Type (max v₁ v₂ u_1)<VAR>I₁ : AddCommMonoid Q<VAR>I₂ I₃ : Module R Q<VAR>I₄ : IsScalarTower R R Q<VAR>g : M →ₗ[R] Q<VAR>this : I₂ = I₃<GOAL>∃! g', ↑R g' ∘ₗ ↑e = g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s t : Finset α<VAR>n : ℕ<VAR>h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t<GOAL>mulRothNumber s < n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s t✝ : Finset α<VAR>n : ℕ<VAR>h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t<VAR>t : Finset α<VAR>hts : t ⊆ s<VAR>hcard : t.card = mulRothNumber s<VAR>ht : ThreeGPFree ↑t<GOAL>mulRothNumber s < n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s t✝ : Finset α<VAR>n : ℕ<VAR>h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t<VAR>t : Finset α<VAR>hts : t ⊆ s<VAR>hcard : t.card = mulRothNumber s<VAR>ht : ThreeGPFree ↑t<GOAL>¬n ≤ t.card
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s t✝ : Finset α<VAR>n : ℕ<VAR>h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ↑t<VAR>t : Finset α<VAR>hts : t ⊆ s<VAR>hcard : t.card = mulRothNumber s<VAR>ht : ThreeGPFree ↑t<VAR>hn : n ≤ t.card<GOAL>False
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s t✝ t : Finset α<VAR>hts : t ⊆ s<VAR>hcard : t.card = mulRothNumber s<VAR>ht : ThreeGPFree ↑t<VAR>u : Finset α<VAR>hut : u ⊆ t<VAR>h : ∀ t ∈ powersetCard u.card s, ¬ThreeGPFree ↑t<VAR>hn : u.card ≤ t.card<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>x : E<GOAL>(reflection K) x = x ↔ x ∈ K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>x : E<GOAL>2 • ↑((orthogonalProjection K) x) = 2 • x ↔ ↑((orthogonalProjection K) x) = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>x : E<GOAL>2 ≠ 0
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>hbdd : BddBelow (range fun n => u n / ↑n)<GOAL>Tendsto (fun n => u n / ↑n) atTop (𝓝 h.lim)
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>hbdd : BddBelow (range fun n => u n / ↑n)<VAR>l : ℝ<VAR>hl : l < h.lim<GOAL>∀ᶠ (b : ℕ) in atTop, l < u b / ↑b
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>hbdd : BddBelow (range fun n => u n / ↑n)<VAR>L : ℝ<VAR>hL : L > h.lim<GOAL>∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
<VAR>R : Type u_1<VAR>n : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>d : n → R<VAR>μ : R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>b : Basis n R M<GOAL>HasEigenvalue ((toLin b b) (diagonal d)) μ ↔ ∃ i, d i = μ
<VAR>R : Type u_1<VAR>n : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>d : n → R<VAR>μ : R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>b : Basis n R M<VAR>this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)<GOAL>HasEigenvalue ((toLin b b) (diagonal d)) μ ↔ ∃ i, d i = μ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>↑⌈b⌉ ≤ ↑⌈a + b⌉ + 1 - a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>b + 1 ≤ ↑⌈a + b⌉ + 1 - a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>a + b ≤ ↑⌈a + b⌉
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<VAR>z₁ z₂ : FirstObj P X<VAR>h : ∀ (i : I), Pi.π (fun i => P.obj (op (X i))) i z₁ = Pi.π (fun i => P.obj (op (X i))) i z₂<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<VAR>z₁ z₂ : FirstObj P X<VAR>h : ∀ (i : I), Pi.π (fun i => P.obj (op (X i))) i z₁ = Pi.π (fun i => P.obj (op (X i))) i z₂<GOAL>∀ (j : Discrete I), limit.π (Discrete.functor fun i => P.obj (op (X i))) j z₁ = limit.π (Discrete.functor fun i => P.obj (op (X i))) j z₂
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ ν : ProbabilityMeasure Ω<VAR>h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s<GOAL>μ = ν
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ ν : ProbabilityMeasure Ω<VAR>h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s<GOAL>↑μ = ↑ν
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : IsPushout f g inl inr<VAR>inst✝ : HasPushout f g<GOAL>inl ≫ h.isoPushout.hom = pushout.inl f g
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s✝ t : Set P<VAR>x : P<VAR>s : Set P<GOAL>intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s