ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>CategoryTheory.Limits.HasLimits C<VAR>i j k : D.J<VAR>U : TopologicalSpace.Opens ↑↑(D.U i)<VAR>X' : C<VAR>f' : ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).obj (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U))) ⟶ X'<GOAL>D.opensImagePreimageMap i j U ≫ (D.f j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U))) ≫ f' = (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (Opposite.op U) ≫ AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j k)) (Opposite.unop (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).toPrefunctor.1 (Opposite.unop (Opposite.op U))))) ≫ (D.V (j, k)).presheaf.map (CategoryTheory.eqToHom ⋯) ≫ f'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>CategoryTheory.Limits.HasLimits C<VAR>i : D.J<VAR>U : TopologicalSpace.Opens ↑↑(D.U i)<GOAL>∃ (eq : Opposite.op U = Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι D.diagram.multispan (Opposite.unop (Opposite.op (CategoryTheory.Limits.WalkingMultispan.right i)))).base).obj (⋯.functor.obj U))), D.ιInvApp U ≫ D.diagramOverOpenπ U i = (D.U i).presheaf.map (CategoryTheory.eqToHom eq)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>CategoryTheory.Limits.HasLimits C<VAR>i j : D.J<VAR>U : TopologicalSpace.Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j = D.diagramOverOpenπ U j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>CategoryTheory.Limits.HasLimits C<VAR>i : D.J<VAR>U : TopologicalSpace.Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (CategoryTheory.Limits.limit (D.diagramOverOpen U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>CategoryTheory.Limits.HasLimits C<VAR>x : ↑↑D.glued<GOAL>∃ i y, (D.ι i).base y = x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : AlgebraicGeometry.SheafedSpace.GlueData C<VAR>i j : self.J<GOAL>AlgebraicGeometry.SheafedSpace.IsOpenImmersion (self.f i j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.SheafedSpace.GlueData C<VAR>CategoryTheory.Limits.HasLimits C<VAR>i : D.J<GOAL>D.toPresheafedSpaceGlueData.ι i ≫ D.isoPresheafedSpace.inv = D.ι i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.SheafedSpace.GlueData C<VAR>CategoryTheory.Limits.HasLimits C<VAR>x : ↑↑D.glued.toPresheafedSpace<GOAL>∃ i y, (D.ι i).base y = x
<VAR>self : AlgebraicGeometry.LocallyRingedSpace.GlueData<VAR>i j : self.J<GOAL>AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (self.f i j)
<VAR>D : AlgebraicGeometry.LocallyRingedSpace.GlueData<VAR>i : D.J<GOAL>D.toSheafedSpaceGlueData.ι i ≫ D.isoSheafedSpace.inv = (D.ι i).val
<VAR>D : AlgebraicGeometry.LocallyRingedSpace.GlueData<VAR>x : ↑D.glued.toTopCat<GOAL>∃ i y, (D.ι i).val.base y = x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>(nilradical R).IsPrime<VAR>CommRing S<VAR>IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>hi : Irreducible (Polynomial.map φ f)<GOAL>Irreducible f
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>H : IsCoprime x y<GOAL>IsCoprime y x
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<GOAL>IsCoprime x y ↔ IsCoprime y x
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<GOAL>IsCoprime x x ↔ IsUnit x
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<GOAL>IsCoprime 0 x ↔ IsUnit x
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<GOAL>IsCoprime x 0 ↔ IsUnit x
<VAR>R : Type u<VAR>CommSemiring R<VAR>Nontrivial R<GOAL>¬IsCoprime 0 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : ℤ<VAR>h : IsCoprime a b<GOAL>IsCoprime ↑a ↑b
<VAR>R : Type u<VAR>CommSemiring R<VAR>Nontrivial R<VAR>p : Fin 2 → R<VAR>h : IsCoprime (p 0) (p 1)<GOAL>p ≠ 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>Nontrivial R<VAR>h : IsCoprime x y<GOAL>x ≠ 0 ∨ y ≠ 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<GOAL>IsCoprime 1 x
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<GOAL>IsCoprime x 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>H1 : IsCoprime x z<VAR>H2 : x ∣ y * z<GOAL>x ∣ y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>H1 : IsCoprime x y<VAR>H2 : x ∣ y * z<GOAL>x ∣ z
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>H1 : IsCoprime x z<VAR>H2 : IsCoprime y z<GOAL>IsCoprime (x * y) z
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>H1 : IsCoprime x y<VAR>H2 : IsCoprime x z<GOAL>IsCoprime x (y * z)
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime x y<VAR>H1 : x ∣ z<VAR>H2 : y ∣ z<GOAL>x * y ∣ z
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime (x * y) z<GOAL>IsCoprime x z
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime (x * y) z<GOAL>IsCoprime y z
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime x (y * z)<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime x (y * z)<GOAL>IsCoprime x z
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<GOAL>IsCoprime (x * y) z ↔ IsCoprime x z ∧ IsCoprime y z
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<GOAL>IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime y z<VAR>hdvd : x ∣ y<GOAL>IsCoprime x z
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime z y<VAR>hdvd : x ∣ y<GOAL>IsCoprime z x
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>H : IsCoprime x y<VAR>d : x ∣ y<GOAL>IsUnit x
<VAR>R : Type u<VAR>CommSemiring R<VAR>a b x : R<VAR>h : IsCoprime a b<VAR>ha : x ∣ a<VAR>hb : x ∣ b<GOAL>IsUnit x
<VAR>R : Type u<VAR>CommSemiring R<VAR>a b : R<VAR>h : IsCoprime a b<GOAL>IsRelPrime a b
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>H : IsCoprime x y<VAR>S : Type v<VAR>CommSemiring S<VAR>f : R →+* S<GOAL>IsCoprime (f x) (f y)
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime (x + y * z) y<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime (x + z * y) y<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime x (y + x * z)<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime x (y + z * x)<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime (y * z + x) y<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime (z * y + x) y<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime x (x * z + y)<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime x (z * x + y)<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsRelPrime (x + y * z) y<GOAL>IsRelPrime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsRelPrime (x + z * y) y<GOAL>IsRelPrime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsRelPrime x (y + x * z)<GOAL>IsRelPrime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsRelPrime x (y + z * x)<GOAL>IsRelPrime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsRelPrime (y * z + x) y<GOAL>IsRelPrime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsRelPrime (z * y + x) y<GOAL>IsRelPrime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsRelPrime x (x * z + y)<GOAL>IsRelPrime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y z : R<VAR>h : IsRelPrime x (z * x + y)<GOAL>IsRelPrime x y
<VAR>R : Type u_1<VAR>G : Type u_2<VAR>CommSemiring R<VAR>Group G<VAR>MulAction G R<VAR>SMulCommClass G R R<VAR>IsScalarTower G R R<VAR>x : G<VAR>y z : R<GOAL>IsCoprime (x • y) z ↔ IsCoprime y z
<VAR>R : Type u_1<VAR>G : Type u_2<VAR>CommSemiring R<VAR>Group G<VAR>MulAction G R<VAR>SMulCommClass G R R<VAR>IsScalarTower G R R<VAR>x : G<VAR>y z : R<GOAL>IsCoprime y (x • z) ↔ IsCoprime y z
<VAR>R : Type u_1<VAR>G : Type u_2<VAR>CommSemiring R<VAR>Group G<VAR>MulAction G R<VAR>SMulCommClass G R R<VAR>IsScalarTower G R R<VAR>x : G<VAR>y z : R<GOAL>IsCoprime (x • y) (x • z) ↔ IsCoprime y z
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x : R<VAR>hu : IsUnit x<VAR>y z : R<GOAL>IsCoprime (x * y) z ↔ IsCoprime y z
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x : R<VAR>hu : IsUnit x<VAR>y z : R<GOAL>IsCoprime y (x * z) ↔ IsCoprime y z
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x : R<VAR>hu : IsUnit x<VAR>y z : R<GOAL>IsCoprime (x * y) (x * z) ↔ IsCoprime y z
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x : R<VAR>hu : IsUnit x<VAR>y z : R<GOAL>IsCoprime (y * x) z ↔ IsCoprime y z
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x : R<VAR>hu : IsUnit x<VAR>y z : R<GOAL>IsCoprime y (z * x) ↔ IsCoprime y z
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x : R<VAR>hu : IsUnit x<VAR>y z : R<GOAL>IsCoprime (y * x) (z * x) ↔ IsCoprime y z
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime (x + y * z) y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime (x + z * y) y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime x (y + x * z)
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime x (y + z * x)
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime (y * z + x) y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime (z * y + x) y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime x (x * z + y)
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime x (z * x + y)
<VAR>R : Type u<VAR>CommRing R<VAR>x y z : R<GOAL>IsCoprime (x + y * z) y ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y z : R<GOAL>IsCoprime (x + z * y) y ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y z : R<GOAL>IsCoprime x (y + x * z) ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y z : R<GOAL>IsCoprime x (y + z * x) ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y z : R<GOAL>IsCoprime (y * z + x) y ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y z : R<GOAL>IsCoprime (z * y + x) y ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y z : R<GOAL>IsCoprime x (x * z + y) ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y z : R<GOAL>IsCoprime x (z * x + y) ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<GOAL>IsCoprime (-x) y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<GOAL>IsCoprime (-x) y ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<GOAL>IsCoprime x (-y)
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<GOAL>IsCoprime x (-y) ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<GOAL>IsCoprime (-x) (-y)
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<GOAL>IsCoprime (-x) (-y) ↔ IsCoprime x y
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>a b : R<VAR>h : IsCoprime a b<GOAL>a ^ 2 + b ^ 2 ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>z : R<VAR>h : IsRelPrime x y<GOAL>IsRelPrime (x + y * z) y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>h : IsRelPrime x y<VAR>z : R<GOAL>IsRelPrime (x + z * y) y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>h : IsRelPrime x y<VAR>z : R<GOAL>IsRelPrime x (y + x * z)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>h : IsRelPrime x y<VAR>z : R<GOAL>IsRelPrime x (y + z * x)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>h : IsRelPrime x y<VAR>z : R<GOAL>IsRelPrime (y * z + x) y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>h : IsRelPrime x y<VAR>z : R<GOAL>IsRelPrime (z * y + x) y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>h : IsRelPrime x y<VAR>z : R<GOAL>IsRelPrime x (x * z + y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>h : IsRelPrime x y<VAR>z : R<GOAL>IsRelPrime x (z * x + y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y z : R<GOAL>IsRelPrime (x + y * z) y ↔ IsRelPrime x y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y z : R<GOAL>IsRelPrime (x + z * y) y ↔ IsRelPrime x y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y z : R<GOAL>IsRelPrime x (y + x * z) ↔ IsRelPrime x y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y z : R<GOAL>IsRelPrime x (y + z * x) ↔ IsRelPrime x y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y z : R<GOAL>IsRelPrime (y * z + x) y ↔ IsRelPrime x y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y z : R<GOAL>IsRelPrime (z * y + x) y ↔ IsRelPrime x y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y z : R<GOAL>IsRelPrime x (x * z + y) ↔ IsRelPrime x y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y z : R<GOAL>IsRelPrime x (z * x + y) ↔ IsRelPrime x y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>h : IsRelPrime x y<GOAL>IsRelPrime (-x) y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>h : IsRelPrime x y<GOAL>IsRelPrime x (-y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>h : IsRelPrime x y<GOAL>IsRelPrime (-x) (-y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<GOAL>IsRelPrime (-x) y ↔ IsRelPrime x y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<GOAL>IsRelPrime x (-y) ↔ IsRelPrime x y
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<GOAL>IsRelPrime (-x) (-y) ↔ IsRelPrime x y
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>MeasureTheory.SigmaFiniteFiltration μ 𝒢<VAR>hf : MeasureTheory.Submartingale f 𝒢 μ<VAR>hτ : MeasureTheory.IsStoppingTime 𝒢 τ<VAR>hπ : MeasureTheory.IsStoppingTime 𝒢 π<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<GOAL>∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hadp : MeasureTheory.Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (τ π : Ω → ℕ), MeasureTheory.IsStoppingTime 𝒢 τ → MeasureTheory.IsStoppingTime 𝒢 π → τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ N) → ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ<GOAL>MeasureTheory.Submartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hadp : MeasureTheory.Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ<GOAL>MeasureTheory.Submartingale f 𝒢 μ ↔ ∀ (τ π : Ω → ℕ), MeasureTheory.IsStoppingTime 𝒢 τ → MeasureTheory.IsStoppingTime 𝒢 π → τ ≤ π → (∃ N, ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ : Ω → ℕ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h : MeasureTheory.Submartingale f 𝒢 μ<VAR>hτ : MeasureTheory.IsStoppingTime 𝒢 τ<GOAL>MeasureTheory.Submartingale (MeasureTheory.stoppedProcess f τ) 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hsub : MeasureTheory.Submartingale f 𝒢 μ<VAR>ε : ℝ≥0<VAR>n : ℕ<GOAL>ε • μ {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω} ≤ ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω}, MeasureTheory.stoppedValue f (MeasureTheory.hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hsub : MeasureTheory.Submartingale f 𝒢 μ<VAR>hnonneg : 0 ≤ f<VAR>ε : ℝ≥0<VAR>n : ℕ<GOAL>ε • μ {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω} ≤ ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω}, f n ω ∂μ)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra A B<VAR>Algebra R B<VAR>IsScalarTower R A B<VAR>x : B<VAR>p : R[X]<GOAL>(Polynomial.aeval x) (Polynomial.map (algebraMap R A) p) = (Polynomial.aeval x) p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>P : R[X]<VAR>a : A<GOAL>Polynomial.eval a (Polynomial.map (algebraMap R A) P) = (Polynomial.aeval a) P
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra A B<VAR>Algebra R B<VAR>IsScalarTower R A B<VAR>x : A<VAR>p : R[X]<GOAL>(Polynomial.aeval ((algebraMap A B) x)) p = (algebraMap A B) ((Polynomial.aeval x) p)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra A B<VAR>Algebra R B<VAR>IsScalarTower R A B<VAR>NoZeroSMulDivisors A B<VAR>Nontrivial B<VAR>x : A<VAR>p : R[X]<GOAL>(Polynomial.aeval ((algebraMap A B) x)) p = 0 ↔ (Polynomial.aeval x) p = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra A B<VAR>Algebra R B<VAR>IsScalarTower R A B<VAR>x : A<VAR>p : R[X]<VAR>h : Function.Injective ⇑(algebraMap A B)<GOAL>(Polynomial.aeval ((algebraMap A B) x)) p = 0 ↔ (Polynomial.aeval x) p = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : ↥S<VAR>p : R[X]<GOAL>(Polynomial.aeval ↑x) p = ↑((Polynomial.aeval x) p)
<VAR>n : ℕ<VAR>z : ℂ<GOAL>¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0)
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<GOAL>Irreducible (Polynomial.X ^ n - Polynomial.X - 1)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hX : MeasureTheory.Memℒp X 2 μ<GOAL>ProbabilityTheory.evariance X μ < ⊤
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hXm : MeasureTheory.AEStronglyMeasurable X μ<VAR>hX : ¬MeasureTheory.Memℒp X 2 μ<GOAL>ProbabilityTheory.evariance X μ = ⊤
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hX : MeasureTheory.AEStronglyMeasurable X μ<GOAL>ProbabilityTheory.evariance X μ < ⊤ ↔ MeasureTheory.Memℒp X 2 μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hX : MeasureTheory.Memℒp X 2 μ<GOAL>ENNReal.ofReal (ProbabilityTheory.variance X μ) = ProbabilityTheory.evariance X μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.evariance X μ = ∫⁻ (ω : Ω), ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2) ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>hX : MeasureTheory.Memℒp X 2 μ<VAR>hXint : ∫ (x : Ω), X x ∂μ = 0<GOAL>ProbabilityTheory.variance X μ = ∫ (x : Ω), (X ^ 2) x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hX : MeasureTheory.Memℒp X 2 μ<GOAL>ProbabilityTheory.variance X μ = ∫ (x : Ω), ((X - fun x => ∫ (x : Ω), X x ∂μ) ^ 2) x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.evariance 0 μ = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<VAR>hX : AEMeasurable X μ<GOAL>ProbabilityTheory.evariance X μ = 0 ↔ X =ᵐ[μ] fun x => ∫ (x : Ω), X x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.evariance (fun ω => c * X ω) μ = ENNReal.ofReal (c ^ 2) * ProbabilityTheory.evariance X μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.variance 0 μ = 0
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<GOAL>0 ≤ ProbabilityTheory.variance X μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.variance (fun ω => c * X ω) μ = c ^ 2 * ProbabilityTheory.variance X μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.variance (c • X) μ = c ^ 2 * ProbabilityTheory.variance X μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>A : Type u_2<VAR>CommSemiring A<VAR>Algebra A ℝ<VAR>c : A<VAR>X : Ω → ℝ<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.variance (c • X) μ = c ^ 2 • ProbabilityTheory.variance X μ
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : MeasureTheory.Memℒp X 2 ℙ<GOAL>ProbabilityTheory.variance X ℙ = (∫ (a : Ω), (X ^ 2) a) - (∫ (a : Ω), X a) ^ 2
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hm : MeasureTheory.AEStronglyMeasurable X ℙ<GOAL>ProbabilityTheory.variance X ℙ ≤ ∫ (a : Ω), (X ^ 2) a
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : MeasureTheory.AEStronglyMeasurable X ℙ<GOAL>ProbabilityTheory.evariance X ℙ = (∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2)) - ENNReal.ofReal ((∫ (a : Ω), X a) ^ 2)
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : MeasureTheory.AEStronglyMeasurable X ℙ<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<GOAL>ℙ {ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} ≤ ProbabilityTheory.evariance X ℙ / ↑c ^ 2
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : MeasureTheory.Memℒp X 2 ℙ<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>ℙ {ω | c ≤ |X ω - ∫ (a : Ω), X a|} ≤ ENNReal.ofReal (ProbabilityTheory.variance X ℙ / c ^ 2)
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : MeasureTheory.Memℒp X 2 ℙ<VAR>hY : MeasureTheory.Memℒp Y 2 ℙ<VAR>h : ProbabilityTheory.IndepFun X Y ℙ<GOAL>ProbabilityTheory.variance (X + Y) ℙ = ProbabilityTheory.variance X ℙ + ProbabilityTheory.variance Y ℙ
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>ι : Type u_2<VAR>X : ι → Ω → ℝ<VAR>s : Finset ι<VAR>hs : ∀ i ∈ s, MeasureTheory.Memℒp (X i) 2 ℙ<VAR>h : (↑s).Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) ℙ<GOAL>ProbabilityTheory.variance (∑ i ∈ s, X i) ℙ = ∑ i ∈ s, ProbabilityTheory.variance (X i) ℙ
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>hab : a < b<VAR>hω : MeasureTheory.upcrossings a b f ω ≠ ⊤<GOAL>¬((∃ᶠ (n : ℕ) in Filter.atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in Filter.atTop, b < f n ω)
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>hab : a < b<VAR>h₁ : ∃ᶠ (n : ℕ) in Filter.atTop, f n ω < a<VAR>h₂ : ∃ᶠ (n : ℕ) in Filter.atTop, b < f n ω<GOAL>MeasureTheory.upcrossings a b f ω = ⊤
<VAR>Ω : Type u_1<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>hf₁ : Filter.liminf (fun n => ↑‖f n ω‖₊) Filter.atTop < ⊤<VAR>hf₂ : ∀ (a b : ℚ), a < b → MeasureTheory.upcrossings (↑a) (↑b) f ω < ⊤<GOAL>∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>R : ℝ≥0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) 1 μ ≤ ↑R<VAR>hab : a < b<GOAL>∀ᵐ (ω : Ω) ∂μ, MeasureTheory.upcrossings a b f ω < ⊤
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>R : ℝ≥0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) 1 μ ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, ∀ (a b : ℚ), a < b → MeasureTheory.upcrossings (↑a) (↑b) f ω < ⊤