ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : Ω → E<VAR>Filter.atTop.IsCountablyGenerated<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>hτ : MeasureTheory.IsStoppingTime ℱ τ<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<VAR>i : ι<GOAL>μ[f|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] μ[f|↑ℱ i]
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : Ω → E<VAR>Filter.atTop.IsCountablyGenerated<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>MeasurableSpace ι<VAR>SecondCountableTopology ι<VAR>BorelSpace ι<VAR>hτ : MeasureTheory.IsStoppingTime ℱ τ<VAR>hσ : MeasureTheory.IsStoppingTime ℱ σ<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<GOAL>μ[f|⋯.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[f|hτ.measurableSpace]
<GOAL>RingHom.StableUnderComposition @RingHom.FiniteType
<GOAL>RingHom.HoldsForLocalizationAway @RingHom.FiniteType
<GOAL>RingHom.OfLocalizationSpanTarget @RingHom.FiniteType
<GOAL>RingHom.PropertyIsLocal @RingHom.FiniteType
<GOAL>RingHom.RespectsIso @RingHom.FiniteType
<GOAL>RingHom.StableUnderBaseChange @RingHom.FiniteType
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>r : R<GOAL>r ∈ v.integer ↔ v r ≤ 1
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>CommRing R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O R<VAR>self : v.Integers O<VAR>r : R<GOAL>v r ≤ 1 → ∃ x, (algebraMap O R) x = r
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>CommRing R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O R<VAR>self : v.Integers O<VAR>x : O<GOAL>v ((algebraMap O R) x) ≤ 1
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>CommRing R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O R<VAR>self : v.Integers O<GOAL>Function.Injective ⇑(algebraMap O R)
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>CommRing R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>v.Integers ↥v.integer
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>CommRing R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O R<VAR>x : O<VAR>hx : IsUnit x<VAR>H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1<GOAL>v ((algebraMap O R) x) = 1
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>CommRing R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O R<VAR>hv : v.Integers O<VAR>x : O<VAR>hx : IsUnit x<GOAL>v ((algebraMap O R) x) = 1
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>CommRing R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O R<VAR>hv : v.Integers O<VAR>x : O<VAR>hx : IsUnit ((algebraMap O R) x)<VAR>hvx : v ((algebraMap O R) x) = 1<GOAL>IsUnit x
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>CommRing R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O R<VAR>hv : v.Integers O<VAR>x y : O<VAR>h : x ∣ y<GOAL>v ((algebraMap O R) y) ≤ v ((algebraMap O R) x)
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>Field F<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O F<VAR>hv : v.Integers O<VAR>x y : O<VAR>h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)<GOAL>y ∣ x
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>Field F<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O F<VAR>hv : v.Integers O<VAR>x y : O<GOAL>x ∣ y ↔ v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>Field F<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O F<VAR>hv : v.Integers O<VAR>x y : O<GOAL>v ((algebraMap O F) x) ≤ v ((algebraMap O F) y) ↔ y ∣ x
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>Field F<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O F<VAR>hv : v.Integers O<VAR>x : O<VAR>hvx : v ((algebraMap O F) x) = 1<GOAL>IsUnit x
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>Field F<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O F<VAR>hv : v.Integers O<VAR>x : F<GOAL>∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a
<VAR>A : Type u_1<VAR>CommRing A<VAR>Γ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ<VAR>v : Valuation A Γ<VAR>S : Submonoid A<VAR>hS : S ≤ v.supp.primeCompl<VAR>B : Type u_3<VAR>CommRing B<VAR>Algebra A B<VAR>IsLocalization S B<VAR>a : A<GOAL>(v.extendToLocalization hS B) ((algebraMap A B) a) = v a
<VAR>R : Type u_1<VAR>CommRing R<VAR>n ν : ℕ<VAR>h : n < ν<GOAL>bernsteinPolynomial R n ν = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>n ν : ℕ<GOAL>Polynomial.map f (bernsteinPolynomial R n ν) = bernsteinPolynomial S n ν
<VAR>R : Type u_1<VAR>CommRing R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>(bernsteinPolynomial R n ν).comp (1 - Polynomial.X) = bernsteinPolynomial R n (n - ν)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>bernsteinPolynomial R n ν = (bernsteinPolynomial R n (n - ν)).comp (1 - Polynomial.X)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n ν : ℕ<GOAL>Polynomial.eval 0 (bernsteinPolynomial R n ν) = if ν = 0 then 1 else 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>n ν : ℕ<GOAL>Polynomial.eval 1 (bernsteinPolynomial R n ν) = if ν = n then 1 else 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>n ν : ℕ<GOAL>Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) = (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
<VAR>R : Type u_1<VAR>CommRing R<VAR>n ν : ℕ<GOAL>Polynomial.derivative (bernsteinPolynomial R n (ν + 1)) = ↑n * (bernsteinPolynomial R (n - 1) ν - bernsteinPolynomial R (n - 1) (ν + 1))
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<GOAL>Polynomial.derivative (bernsteinPolynomial R n 0) = -↑n * bernsteinPolynomial R (n - 1) 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>ν k : ℕ<GOAL>k < ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>n ν : ℕ<GOAL>Polynomial.eval 0 ((⇑Polynomial.derivative)^[ν] (bernsteinPolynomial R n (ν + 1))) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>n ν : ℕ<GOAL>Polynomial.eval 0 ((⇑Polynomial.derivative)^[ν] (bernsteinPolynomial R n ν)) = Polynomial.eval (↑(n - (ν - 1))) (ascPochhammer R ν)
<VAR>R : Type u_1<VAR>CommRing R<VAR>CharZero R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>Polynomial.eval 0 ((⇑Polynomial.derivative)^[ν] (bernsteinPolynomial R n ν)) ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>ν k : ℕ<GOAL>k < n - ν → Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>Polynomial.eval 1 ((⇑Polynomial.derivative)^[n - ν] (bernsteinPolynomial R n ν)) = (-1) ^ (n - ν) * Polynomial.eval (↑ν + 1) (ascPochhammer R (n - ν))
<VAR>R : Type u_1<VAR>CommRing R<VAR>CharZero R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>Polynomial.eval 1 ((⇑Polynomial.derivative)^[n - ν] (bernsteinPolynomial R n ν)) ≠ 0
<VAR>n k : ℕ<VAR>h : k ≤ n + 1<GOAL>LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
<VAR>n : ℕ<GOAL>LinearIndependent ℚ fun ν => bernsteinPolynomial ℚ n ↑ν
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<GOAL>∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<GOAL>∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • Polynomial.X
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<GOAL>∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • Polynomial.X ^ 2
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<GOAL>∑ ν ∈ Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • Polynomial.X * (1 - Polynomial.X)
<VAR>R : Type u_1<VAR>Ring R<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>self : v.RankOne<GOAL>∃ r, v r ≠ 0 ∧ v r ≠ 1
<VAR>R : Type u_1<VAR>Ring R<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>self : v.RankOne<GOAL>StrictMono ⇑(Valuation.RankOne.hom v)
<VAR>R : Type u_1<VAR>Ring R<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>v.RankOne<GOAL>StrictMono ⇑(Valuation.RankOne.hom v)
<VAR>R : Type u_1<VAR>Ring R<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>v.RankOne<GOAL>∃ r, v r ≠ 0 ∧ v r ≠ 1
<VAR>R : Type u_1<VAR>Ring R<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>v.RankOne<VAR>x : Γ₀<VAR>hx : (Valuation.RankOne.hom v) x = 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>v.RankOne<VAR>x : Γ₀<GOAL>(Valuation.RankOne.hom v) x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>Γ₀ : Type u_2<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>v.RankOne<GOAL>Valuation.RankOne.unit v ≠ 1
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>CommRing R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O R<VAR>hv : v.Integers O<VAR>x : R<VAR>hx : IsIntegral O x<GOAL>x ∈ v.integer
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>CommRing R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O R<VAR>hv : v.Integers O<GOAL>integralClosure O R = ⊥
<VAR>K : Type u<VAR>Γ₀ : Type v<VAR>Field K<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>O : Type w<VAR>CommRing O<VAR>Algebra O K<VAR>IsFractionRing O K<VAR>hv : v.Integers O<GOAL>IsIntegrallyClosed O
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : R<VAR>DecidableRel Dvd.dvd<VAR>hp : Prime p<VAR>r : R<GOAL>(multiplicity.addValuation hp) r = multiplicity p r
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>self : HopfAlgebra R A<GOAL>LinearMap.mul' R A ∘ₗ LinearMap.rTensor A HopfAlgebra.antipode ∘ₗ Coalgebra.comul = Algebra.linearMap R A ∘ₗ Coalgebra.counit
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>self : HopfAlgebra R A<GOAL>LinearMap.mul' R A ∘ₗ LinearMap.lTensor A HopfAlgebra.antipode ∘ₗ Coalgebra.comul = Algebra.linearMap R A ∘ₗ Coalgebra.counit
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>HopfAlgebra R A<VAR>a : A<GOAL>(LinearMap.mul' R A) ((LinearMap.rTensor A HopfAlgebra.antipode) (Coalgebra.comul a)) = (algebraMap R A) (Coalgebra.counit a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>HopfAlgebra R A<VAR>a : A<GOAL>(LinearMap.mul' R A) ((LinearMap.lTensor A HopfAlgebra.antipode) (Coalgebra.comul a)) = (algebraMap R A) (Coalgebra.counit a)
<VAR>R : Type u<VAR>CommSemiring R<GOAL>HopfAlgebra.antipode = LinearMap.id
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<VAR>M : Type u_1<VAR>M' : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>x : M<GOAL>((QuotSMulTop.map r) f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<VAR>M : Type u_1<VAR>M' : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<GOAL>(QuotSMulTop.map r) f ∘ₗ (r • ⊤).mkQ = (r • ⊤).mkQ ∘ₗ f
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<GOAL>(QuotSMulTop.map r) LinearMap.id = LinearMap.id
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<VAR>M : Type u_1<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>AddCommGroup M''<VAR>Module R M''<VAR>g : M' →ₗ[R] M''<VAR>f : M →ₗ[R] M'<GOAL>(QuotSMulTop.map r) (g ∘ₗ f) = (QuotSMulTop.map r) g ∘ₗ (QuotSMulTop.map r) f
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<VAR>M : Type u_1<VAR>M' : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>x : M<GOAL>(QuotSMulTop.equivQuotTensor r M') (((QuotSMulTop.map r) f) (Submodule.Quotient.mk x)) = (LinearMap.lTensor (R ⧸ Ideal.span {r}) f) ((QuotSMulTop.equivQuotTensor r M) (Submodule.Quotient.mk x))
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<VAR>M : Type u_1<VAR>M' : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<GOAL>↑(QuotSMulTop.equivQuotTensor r M') ∘ₗ (QuotSMulTop.map r) f = LinearMap.lTensor (R ⧸ Ideal.span {r}) f ∘ₗ ↑(QuotSMulTop.equivQuotTensor r M)
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<VAR>M : Type u_1<VAR>M' : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>x : M<GOAL>(QuotSMulTop.equivTensorQuot r M') (((QuotSMulTop.map r) f) (Submodule.Quotient.mk x)) = (LinearMap.rTensor (R ⧸ Ideal.span {r}) f) ((QuotSMulTop.equivTensorQuot r M) (Submodule.Quotient.mk x))
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<VAR>M : Type u_1<VAR>M' : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<GOAL>↑(QuotSMulTop.equivTensorQuot r M') ∘ₗ (QuotSMulTop.map r) f = LinearMap.rTensor (R ⧸ Ideal.span {r}) f ∘ₗ ↑(QuotSMulTop.equivTensorQuot r M)
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<VAR>M : Type u_1<VAR>M' : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑((QuotSMulTop.map r) f)
<VAR>R : Type u_2<VAR>CommRing R<VAR>r : R<VAR>M : Type u_1<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>AddCommGroup M''<VAR>Module R M''<VAR>f : M →ₗ[R] M'<VAR>g : M' →ₗ[R] M''<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<GOAL>Function.Exact ⇑((QuotSMulTop.map r) f) ⇑((QuotSMulTop.map r) g)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n m : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<GOAL>MvPolynomial.coeff m (MvPowerSeries.truncFun n φ) = if m < n then (MvPowerSeries.coeff R m) φ else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n m : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<GOAL>MvPolynomial.coeff m ((MvPowerSeries.trunc R n) φ) = if m < n then (MvPowerSeries.coeff R m) φ else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n : σ →₀ ℕ<VAR>hnn : n ≠ 0<GOAL>(MvPowerSeries.trunc R n) 1 = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n : σ →₀ ℕ<VAR>hnn : n ≠ 0<VAR>a : R<GOAL>(MvPowerSeries.trunc R n) ((MvPowerSeries.C σ R) a) = MvPolynomial.C a
<VAR>a b : ℤ<GOAL>a.gcd b = 1 ↔ IsCoprime a b
<VAR>a b c : ℤ<VAR>h : IsCoprime a b<VAR>heq : a * b = c ^ 2<GOAL>∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
<VAR>k : ℤ<GOAL>Prime k ↔ Nat.Prime k.natAbs
<VAR>a : ℤ<GOAL>AddSubgroup.zmultiples ↑a.natAbs = AddSubgroup.zmultiples a
<VAR>a : ℤ<GOAL>Ideal.span {↑a.natAbs} = Ideal.span {a}
<VAR>a b c : ℤ<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>hk : Odd k<VAR>h : a * b = c ^ k<GOAL>∃ d, b = d ^ k
<VAR>a b c : ℤ<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>hk : Odd k<VAR>h : a * b = c ^ k<GOAL>(∃ d, a = d ^ k) ∧ ∃ e, b = e ^ k
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>A : ℝ<GOAL>MeasureTheory.AEStronglyMeasurable (ProbabilityTheory.truncation f A) μ
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>A : ℝ<VAR>x : α<GOAL>|ProbabilityTheory.truncation f A x| ≤ |A|
<VAR>α : Type u_1<VAR>f : α → ℝ<GOAL>ProbabilityTheory.truncation f 0 = 0
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>A : ℝ<VAR>x : α<GOAL>|ProbabilityTheory.truncation f A x| ≤ |f x|
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>A : ℝ<VAR>x : α<VAR>h : |f x| < A<GOAL>ProbabilityTheory.truncation f A x = f x
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>A : ℝ<VAR>h : ∀ (x : α), 0 ≤ f x<GOAL>ProbabilityTheory.truncation f A = (Set.Ioc 0 A).indicator id ∘ f
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>A : ℝ<VAR>x : α<VAR>h : 0 ≤ f x<GOAL>0 ≤ ProbabilityTheory.truncation f A x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>p : ℝ≥0∞<GOAL>MeasureTheory.Memℒp (ProbabilityTheory.truncation f A) p μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>A : ℝ<GOAL>MeasureTheory.Integrable (ProbabilityTheory.truncation f A) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>hA : 0 ≤ A<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>∫ (x : α), ProbabilityTheory.truncation f A x ^ n ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂MeasureTheory.Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h'f : 0 ≤ f<GOAL>∫ (x : α), ProbabilityTheory.truncation f A x ^ n ∂μ = ∫ (y : ℝ) in 0 ..A, y ^ n ∂MeasureTheory.Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>hA : 0 ≤ A<GOAL>∫ (x : α), ProbabilityTheory.truncation f A x ∂μ = ∫ (y : ℝ) in -A..A, y ∂MeasureTheory.Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>h'f : 0 ≤ f<GOAL>∫ (x : α), ProbabilityTheory.truncation f A x ∂μ = ∫ (y : ℝ) in 0 ..A, y ∂MeasureTheory.Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>h'f : 0 ≤ f<VAR>A : ℝ<GOAL>∫ (x : α), ProbabilityTheory.truncation f A x ∂μ ≤ ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>Filter.Tendsto (fun A => ∫ (x : α), ProbabilityTheory.truncation f A x ∂μ) Filter.atTop (𝓝 (∫ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>f : α → ℝ<VAR>g : β → ℝ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>A : ℝ<GOAL>ProbabilityTheory.IdentDistrib (ProbabilityTheory.truncation f A) (ProbabilityTheory.truncation g A) μ ν
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : MeasureTheory.Integrable X ℙ<VAR>hnonneg : 0 ≤ X<VAR>K N : ℕ<VAR>hKN : K ≤ N<GOAL>∑ j ∈ Finset.range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : MeasureTheory.Integrable X ℙ<VAR>hnonneg : 0 ≤ X<GOAL>∑' (j : ℕ), ℙ {ω | X ω ∈ Set.Ioi ↑j} < ⊤
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : MeasureTheory.Integrable X ℙ<VAR>hnonneg : 0 ≤ X<VAR>K : ℕ<GOAL>∑ j ∈ Finset.range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (ProbabilityTheory.truncation X ↑j ^ 2) a ≤ 2 * ∫ (a : Ω), X a
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : MeasureTheory.Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in Filter.atTop, |∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) ↑i) a| < ε * ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : MeasureTheory.Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<GOAL>∀ᵐ (ω : Ω), (fun n => ∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) ↑i) a) =o[Filter.atTop] fun n => ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : MeasureTheory.Integrable (X 0) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<GOAL>(fun n => (∫ (a : Ω), (∑ i ∈ Finset.range n, ProbabilityTheory.truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a) =o[Filter.atTop] Nat.cast
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : MeasureTheory.Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<GOAL>∀ᵐ (ω : Ω), (fun n => ∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[Filter.atTop] fun n => ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : MeasureTheory.Integrable (X 0) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<GOAL>∀ᵐ (ω : Ω), (fun n => ∑ i ∈ Finset.range n, ProbabilityTheory.truncation (X i) (↑i) ω - ∑ i ∈ Finset.range n, X i ω) =o[Filter.atTop] fun n => ↑n
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : MeasureTheory.Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<GOAL>∀ᵐ (ω : Ω), Filter.Tendsto (fun n => (∑ i ∈ Finset.range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊) Filter.atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : MeasureTheory.Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<GOAL>∀ᵐ (ω : Ω), Filter.Tendsto (fun n => (∑ i ∈ Finset.range n, X i ω) / ↑n) Filter.atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : MeasureTheory.Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<GOAL>∀ᵐ (ω : Ω), Filter.Tendsto (fun n => (∑ i ∈ Finset.range n, X i ω) / ↑n) Filter.atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>MeasureTheory.MeasureSpace Ω<VAR>MeasureTheory.IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>MeasurableSpace E<VAR>X : ℕ → Ω → E<VAR>h' : Measurable (X 0)<VAR>hindep : Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) ℙ ℙ<VAR>φ : MeasureTheory.SimpleFunc E E<GOAL>∀ᵐ (ω : Ω), Filter.Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, ↑φ (X i ω)) Filter.atTop (𝓝 (∫ (a : Ω), (↑φ ∘ X 0) a))