ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>I : Type u_1<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x : α<VAR>s : I → α<VAR>t : Finset I<GOAL>(∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
<VAR>α : Type u_2<VAR>I : Type u_1<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x : α<VAR>s : I → α<VAR>t : Finset I<GOAL>(∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (∏ i ∈ t, s i)
<VAR>α : Type u_1<VAR>I : Type u_2<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x : α<VAR>s : I → α<VAR>t : Finset I<GOAL>IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
<VAR>α : Type u_1<VAR>I : Type u_2<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x : α<VAR>s : I → α<VAR>t : Finset I<GOAL>IsRelPrime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsRelPrime x (s i)
<VAR>α : Type u_1<VAR>I : Type u_2<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x : α<VAR>s : I → α<VAR>t : Finset I<VAR>H1 : IsRelPrime (∏ i ∈ t, s i) x<VAR>i : I<VAR>hit : i ∈ t<GOAL>IsRelPrime (s i) x
<VAR>α : Type u_1<VAR>I : Type u_2<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x : α<VAR>s : I → α<VAR>t : Finset I<VAR>H1 : IsRelPrime x (∏ i ∈ t, s i)<VAR>i : I<VAR>hit : i ∈ t<GOAL>IsRelPrime x (s i)
<VAR>α : Type u_2<VAR>I : Type u_1<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>z : α<VAR>s : I → α<VAR>t : Finset I<GOAL>(↑t).Pairwise (IsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z
<VAR>α : Type u_2<VAR>I : Type u_1<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>z : α<VAR>s : I → α<VAR>Fintype I<VAR>Hs : Pairwise (IsRelPrime on s)<VAR>Hs1 : ∀ (i : I), s i ∣ z<GOAL>∏ x : I, s x ∣ z
<VAR>α : Type u_2<VAR>I : Type u_1<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>s : I → α<VAR>t : Finset I<VAR>DecidableEq I<GOAL>Pairwise (IsRelPrime on fun i => s ↑i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x y : α<VAR>m : ℕ<VAR>H : IsRelPrime x y<GOAL>IsRelPrime (x ^ m) y
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x y : α<VAR>n : ℕ<VAR>H : IsRelPrime x y<GOAL>IsRelPrime x (y ^ n)
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x y : α<VAR>m n : ℕ<VAR>H : IsRelPrime x y<GOAL>IsRelPrime (x ^ m) (y ^ n)
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x y : α<VAR>m : ℕ<VAR>hm : 0 < m<GOAL>IsRelPrime (x ^ m) y ↔ IsRelPrime x y
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x y : α<VAR>m : ℕ<VAR>hm : 0 < m<GOAL>IsRelPrime x (y ^ m) ↔ IsRelPrime x y
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>DecompositionMonoid α<VAR>x y : α<VAR>m n : ℕ<VAR>hm : 0 < m<VAR>hn : 0 < n<GOAL>IsRelPrime (x ^ m) (y ^ n) ↔ IsRelPrime x y
<VAR>S : Type u<VAR>Semiring S<GOAL>ascPochhammer S 0 = 1
<VAR>S : Type u<VAR>Semiring S<GOAL>ascPochhammer S 1 = Polynomial.X
<VAR>S : Type u<VAR>Semiring S<VAR>n : ℕ<GOAL>ascPochhammer S (n + 1) = Polynomial.X * (ascPochhammer S n).comp (Polynomial.X + 1)
<VAR>S : Type u<VAR>Semiring S<VAR>n : ℕ<VAR>Nontrivial S<VAR>NoZeroDivisors S<GOAL>(ascPochhammer S n).Monic
<VAR>S : Type u<VAR>Semiring S<VAR>T : Type v<VAR>Semiring T<VAR>f : S →+* T<VAR>n : ℕ<GOAL>Polynomial.map f (ascPochhammer S n) = ascPochhammer T n
<VAR>S : Type u<VAR>Semiring S<VAR>T : Type v<VAR>Semiring T<VAR>f : S →+* T<VAR>n : ℕ<VAR>t : T<GOAL>Polynomial.eval t (ascPochhammer T n) = Polynomial.eval₂ f t (ascPochhammer S n)
<VAR>S : Type u<VAR>Semiring S<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : ℕ<VAR>p : R[X]<VAR>Algebra R S<VAR>x : S<GOAL>Polynomial.eval x ((ascPochhammer S n).comp (Polynomial.map (algebraMap R S) p)) = Polynomial.eval (Polynomial.eval₂ (algebraMap R S) x p) (ascPochhammer S n)
<VAR>S : Type u<VAR>Semiring S<VAR>n k : ℕ<GOAL>↑(Polynomial.eval k (ascPochhammer ℕ n)) = Polynomial.eval (↑k) (ascPochhammer S n)
<VAR>S : Type u<VAR>Semiring S<VAR>n : ℕ<GOAL>Polynomial.eval 0 (ascPochhammer S n) = if n = 0 then 1 else 0
<VAR>S : Type u<VAR>Semiring S<GOAL>Polynomial.eval 0 (ascPochhammer S 0) = 1
<VAR>S : Type u<VAR>Semiring S<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Polynomial.eval 0 (ascPochhammer S n) = 0
<VAR>S : Type u<VAR>Semiring S<VAR>n : ℕ<GOAL>ascPochhammer S (n + 1) = ascPochhammer S n * (Polynomial.X + ↑n)
<VAR>S : Type u_1<VAR>Semiring S<VAR>n : ℕ<VAR>k : S<GOAL>Polynomial.eval k (ascPochhammer S (n + 1)) = Polynomial.eval k (ascPochhammer S n) * (k + ↑n)
<VAR>S : Type u<VAR>Semiring S<VAR>n : ℕ<GOAL>(ascPochhammer S (n + 1)).comp (Polynomial.X + 1) = ascPochhammer S (n + 1) + (n + 1) • (ascPochhammer S n).comp (Polynomial.X + 1)
<VAR>S : Type u<VAR>Semiring S<VAR>n m : ℕ<GOAL>ascPochhammer S n * (ascPochhammer S m).comp (Polynomial.X + ↑n) = ascPochhammer S (n + m)
<VAR>n k : ℕ<GOAL>Polynomial.eval n (ascPochhammer ℕ k) = n.ascFactorial k
<VAR>a b : ℕ<GOAL>Polynomial.eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b
<VAR>S : Type u<VAR>Semiring S<VAR>n : ℕ<VAR>NoZeroDivisors S<VAR>Nontrivial S<GOAL>(ascPochhammer S n).natDegree = n
<VAR>S : Type u_1<VAR>StrictOrderedSemiring S<VAR>n : ℕ<VAR>s : S<VAR>h : 0 < s<GOAL>0 < Polynomial.eval s (ascPochhammer S n)
<VAR>S : Type u_2<VAR>Semiring S<VAR>n : ℕ<GOAL>Polynomial.eval 1 (ascPochhammer S n) = ↑n.factorial
<VAR>S : Type u_2<VAR>Semiring S<VAR>r n : ℕ<GOAL>↑r.factorial * Polynomial.eval (↑r + 1) (ascPochhammer S n) = ↑(r + n).factorial
<VAR>r n : ℕ<GOAL>n * Polynomial.eval (n + 1) (ascPochhammer ℕ r) = (n + r) * Polynomial.eval n (ascPochhammer ℕ r)
<VAR>S : Type u_1<VAR>Semiring S<VAR>r n : ℕ<GOAL>↑n * Polynomial.eval (↑n + 1) (ascPochhammer S r) = (↑n + ↑r) * Polynomial.eval (↑n) (ascPochhammer S r)
<VAR>R : Type u<VAR>Ring R<GOAL>descPochhammer R 0 = 1
<VAR>R : Type u<VAR>Ring R<GOAL>descPochhammer R 1 = Polynomial.X
<VAR>R : Type u<VAR>Ring R<VAR>n : ℕ<GOAL>descPochhammer R (n + 1) = Polynomial.X * (descPochhammer R n).comp (Polynomial.X - 1)
<VAR>R : Type u<VAR>Ring R<VAR>n : ℕ<VAR>Nontrivial R<VAR>NoZeroDivisors R<GOAL>(descPochhammer R n).Monic
<VAR>R : Type u<VAR>Ring R<VAR>T : Type v<VAR>Ring T<VAR>f : R →+* T<VAR>n : ℕ<GOAL>Polynomial.map f (descPochhammer R n) = descPochhammer T n
<VAR>R : Type u<VAR>Ring R<VAR>n : ℕ<VAR>k : ℤ<GOAL>↑(Polynomial.eval k (descPochhammer ℤ n)) = Polynomial.eval (↑k) (descPochhammer R n)
<VAR>R : Type u<VAR>Ring R<VAR>n : ℕ<GOAL>Polynomial.eval 0 (descPochhammer R n) = if n = 0 then 1 else 0
<VAR>R : Type u<VAR>Ring R<GOAL>Polynomial.eval 0 (descPochhammer R 0) = 1
<VAR>R : Type u<VAR>Ring R<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Polynomial.eval 0 (descPochhammer R n) = 0
<VAR>R : Type u<VAR>Ring R<VAR>n : ℕ<GOAL>descPochhammer R (n + 1) = descPochhammer R n * (Polynomial.X - ↑n)
<VAR>R : Type u<VAR>Ring R<VAR>n : ℕ<VAR>NoZeroDivisors R<VAR>Nontrivial R<GOAL>(descPochhammer R n).natDegree = n
<VAR>S : Type u_1<VAR>Ring S<VAR>n : ℕ<VAR>k : S<GOAL>Polynomial.eval k (descPochhammer S (n + 1)) = Polynomial.eval k (descPochhammer S n) * (k - ↑n)
<VAR>R : Type u<VAR>Ring R<VAR>n : ℕ<GOAL>(descPochhammer R (n + 1)).comp (Polynomial.X - 1) = descPochhammer R (n + 1) - (↑n + 1) • (descPochhammer R n).comp (Polynomial.X - 1)
<VAR>n : ℕ<GOAL>descPochhammer ℤ n = (ascPochhammer ℤ n).comp (Polynomial.X - ↑n + 1)
<VAR>R : Type u<VAR>Ring R<VAR>r : R<VAR>n : ℕ<GOAL>Polynomial.eval r (descPochhammer R n) = Polynomial.eval (r - ↑n + 1) (ascPochhammer R n)
<VAR>R : Type u<VAR>Ring R<VAR>n m : ℕ<GOAL>descPochhammer R n * (descPochhammer R m).comp (Polynomial.X - ↑n) = descPochhammer R (n + m)
<VAR>R : Type u<VAR>Ring R<VAR>r : R<VAR>k : ℕ<GOAL>Polynomial.eval (-r) (ascPochhammer R k) = (-1) ^ k * Polynomial.eval r (descPochhammer R k)
<VAR>R : Type u<VAR>Ring R<VAR>n k : ℕ<GOAL>Polynomial.eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
<VAR>a b : ℕ<GOAL>Polynomial.eval (↑a + ↑b) (descPochhammer ℤ b) = ↑((a + 1).ascFactorial b)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>s : Multiset R<GOAL>(Multiset.map (fun r => Polynomial.X + Polynomial.C r) s).prod = ∑ j ∈ Finset.range (Multiset.card s + 1), Polynomial.C (s.esymm j) * Polynomial.X ^ (Multiset.card s - j)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ Multiset.card s<GOAL>(Multiset.map (fun r => Polynomial.X + Polynomial.C r) s).prod.coeff k = s.esymm (Multiset.card s - k)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>σ : Type u_2<VAR>s : Multiset σ<VAR>r : σ → R<VAR>k : ℕ<VAR>h : k ≤ Multiset.card s<GOAL>(Multiset.map (fun i => Polynomial.X + Polynomial.C (r i)) s).prod.coeff k = (Multiset.map r s).esymm (Multiset.card s - k)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>σ : Type u_2<VAR>s : Finset σ<VAR>r : σ → R<VAR>k : ℕ<VAR>h : k ≤ s.card<GOAL>(∏ i ∈ s, (Polynomial.X + Polynomial.C (r i))).coeff k = ∑ t ∈ Finset.powersetCard (s.card - k) s, ∏ i ∈ t, r i
<VAR>R : Type u_1<VAR>CommRing R<VAR>s : Multiset R<VAR>k : ℕ<GOAL>(Multiset.map Neg.neg s).esymm k = (-1) ^ k * s.esymm k
<VAR>R : Type u_1<VAR>CommRing R<VAR>s : Multiset R<GOAL>(Multiset.map (fun t => Polynomial.X - Polynomial.C t) s).prod = ∑ j ∈ Finset.range (Multiset.card s + 1), (-1) ^ j * (Polynomial.C (s.esymm j) * Polynomial.X ^ (Multiset.card s - j))
<VAR>R : Type u_1<VAR>CommRing R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ Multiset.card s<GOAL>(Multiset.map (fun t => Polynomial.X - Polynomial.C t) s).prod.coeff k = (-1) ^ (Multiset.card s - k) * s.esymm (Multiset.card s - k)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : R[X]<VAR>hroots : Multiset.card p.roots = p.natDegree<VAR>k : ℕ<VAR>h : k ≤ p.natDegree<GOAL>p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
<VAR>F : Type u_2<VAR>Field F<VAR>p : F[X]<VAR>hsplit : Polynomial.Splits (RingHom.id F) p<VAR>k : ℕ<VAR>h : k ≤ p.natDegree<GOAL>p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<GOAL>∏ i : σ, (Polynomial.X + Polynomial.C (MvPolynomial.X i)) = ∑ j ∈ Finset.range (Fintype.card σ + 1), Polynomial.C (MvPolynomial.esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>CommSemiring R<VAR>Fintype σ<VAR>k : ℕ<VAR>h : k ≤ Fintype.card σ<GOAL>(∏ i : σ, (Polynomial.X + Polynomial.C (MvPolynomial.X i))).coeff k = MvPolynomial.esymm σ R (Fintype.card σ - k)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>s : R<VAR>i : ℕ<GOAL>(p.scaleRoots s).coeff i = p.coeff i * s ^ (p.natDegree - i)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>s : R<GOAL>(p.scaleRoots s).coeff p.natDegree = p.leadingCoeff
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : R<GOAL>Polynomial.scaleRoots 0 s = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>hp : p ≠ 0<VAR>s : R<GOAL>p.scaleRoots s ≠ 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>s : R<GOAL>(p.scaleRoots s).support ≤ p.support
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>s : R<VAR>hs : s ∈ nonZeroDivisors R<GOAL>(p.scaleRoots s).support = p.support
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>s : R<GOAL>(p.scaleRoots s).degree = p.degree
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>s : R<GOAL>(p.scaleRoots s).natDegree = p.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<VAR>s : R<GOAL>(p.scaleRoots s).Monic ↔ p.Monic
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>p : Polynomial R<VAR>x : R<VAR>f : R →+* S<VAR>h : f p.leadingCoeff ≠ 0<GOAL>Polynomial.map f (p.scaleRoots x) = (Polynomial.map f p).scaleRoots (f x)
<VAR>R : Type u_1<VAR>Semiring R<VAR>r c : R<GOAL>(Polynomial.C c).scaleRoots r = Polynomial.C c
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>p.scaleRoots 1 = p
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : Polynomial R<GOAL>p.scaleRoots 0 = p.leadingCoeff • Polynomial.X ^ p.natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<GOAL>Polynomial.scaleRoots 1 r = 1
<VAR>S : Type u_2<VAR>A : Type u_3<VAR>Semiring S<VAR>Semiring A<VAR>p : Polynomial S<VAR>f : S →+* A<VAR>a : A<VAR>s : S<VAR>hsa : Commute (f s) a<VAR>hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)<GOAL>Polynomial.eval₂ f (f s * a) (p.scaleRoots s) = f s ^ p.natDegree * Polynomial.eval₂ f a p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring S<VAR>CommSemiring R<VAR>p : Polynomial S<VAR>f : S →+* R<VAR>r : R<VAR>s : S<GOAL>Polynomial.eval₂ f (f s * r) (p.scaleRoots s) = f s ^ p.natDegree * Polynomial.eval₂ f r p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring S<VAR>CommSemiring R<VAR>p : Polynomial S<VAR>f : S →+* R<VAR>r : R<VAR>s : S<VAR>hr : Polynomial.eval₂ f r p = 0<GOAL>Polynomial.eval₂ f (f s * r) (p.scaleRoots s) = 0
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>p : Polynomial R<VAR>a : A<VAR>r : R<VAR>ha : (Polynomial.aeval a) p = 0<GOAL>(Polynomial.aeval ((algebraMap R A) r * a)) (p.scaleRoots r) = 0
<VAR>S : Type u_2<VAR>K : Type u_4<VAR>Semiring S<VAR>Field K<VAR>p : Polynomial S<VAR>f : S →+* K<VAR>hf : Function.Injective ⇑f<VAR>r s : S<VAR>hr : Polynomial.eval₂ f (f r / f s) p = 0<VAR>hs : s ∈ nonZeroDivisors S<GOAL>Polynomial.eval₂ f (f r) (p.scaleRoots s) = 0
<VAR>R : Type u_1<VAR>K : Type u_4<VAR>CommSemiring R<VAR>Field K<VAR>Algebra R K<VAR>inj : Function.Injective ⇑(algebraMap R K)<VAR>p : Polynomial R<VAR>r s : R<VAR>hr : (Polynomial.aeval ((algebraMap R K) r / (algebraMap R K) s)) p = 0<VAR>hs : s ∈ nonZeroDivisors R<GOAL>(Polynomial.aeval ((algebraMap R K) r)) (p.scaleRoots s) = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : Polynomial R<VAR>r s : R<GOAL>p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : Polynomial R<VAR>r : R<GOAL>r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : Polynomial R<VAR>r : R<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<GOAL>(p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : Polynomial R<VAR>r : R<VAR>NoZeroDivisors R<GOAL>(p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : Polynomial R<VAR>r : R<VAR>h : p.natDegree = q.natDegree<GOAL>r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r = p.scaleRoots r + q.scaleRoots r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : Polynomial R<VAR>r : R<VAR>hr : IsUnit r<VAR>hpq : p ∣ q<GOAL>p.scaleRoots r ∣ q.scaleRoots r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : Polynomial R<VAR>r : R<VAR>NoZeroDivisors R<VAR>hpq : p ∣ q<GOAL>p.scaleRoots r ∣ q.scaleRoots r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : Polynomial R<VAR>r : R<VAR>hr : IsUnit r<GOAL>p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : Polynomial R<VAR>r : R<VAR>hr : IsUnit r<VAR>h : IsCoprime p q<GOAL>IsCoprime (p.scaleRoots r) (q.scaleRoots r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<GOAL>(fun t => κ.densityProcess ν n a t s) = fun t => ((κ a) (MeasurableSpace.countablePartitionSet n t ×ˢ s) / (ν a) (MeasurableSpace.countablePartitionSet n t)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>n : ℕ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun p => (κ p.1) (MeasurableSpace.countablePartitionSet n p.2 ×ˢ s) / (ν p.1) (MeasurableSpace.countablePartitionSet n p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>n : ℕ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun p => κ.densityProcess ν n p.1 p.2 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>n : ℕ<VAR>x : γ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => κ.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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>n : ℕ<VAR>s : Set β<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => κ.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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => κ.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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.StronglyMeasurable fun x => κ.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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Adapted (ProbabilityTheory.countableFiltration γ) fun n x => κ.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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>0 ≤ κ.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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>(κ a) (MeasurableSpace.countablePartitionSet n x ×ˢ s) ≤ (ν a) (MeasurableSpace.countablePartitionSet n x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>κ.densityProcess ν n a x s ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<GOAL>MeasureTheory.eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) ≤ (ν a) Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Integrable (fun x => κ.densityProcess ν n a x s) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : ProbabilityTheory.IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ MeasurableSpace.countablePartition γ n<GOAL>∫ (x : γ) in u, κ.densityProcess ν n a x s ∂ν a = ((κ a) (u ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<GOAL>∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫ (x : γ), κ.densityProcess ν n a x s ∂ν a = ((κ a) (Set.univ ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>n m : ℕ<VAR>hnm : n ≤ m<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<GOAL>∫ (x : γ) in A, κ.densityProcess ν m a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>ν a[fun x => κ.densityProcess ν j a x s|↑(ProbabilityTheory.countableFiltration γ) i] =ᵐ[ν a] fun x => κ.densityProcess ν i 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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Martingale (fun n x => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s s' : Set β<VAR>h : s ⊆ s'<GOAL>κ.densityProcess ν n a x s ≤ κ.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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>κ' : ProbabilityTheory.Kernel α (γ × β)<VAR>hκκ' : κ ≤ κ'<VAR>hκ'ν : κ'.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>κ.densityProcess ν n a x s ≤ κ'.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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν ν' : ProbabilityTheory.Kernel α γ<VAR>hνν' : ν ≤ ν'<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>κ.densityProcess ν' n a x s ≤ κ.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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<GOAL>κ.densityProcess ν n a x ∅ = 0