ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ η : ProbabilityTheory.Kernel α β<GOAL>ProbabilityTheory.Kernel.prodMkLeft γ (κ + η) = ProbabilityTheory.Kernel.prodMkLeft γ κ + ProbabilityTheory.Kernel.prodMkLeft γ η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ η : ProbabilityTheory.Kernel α β<GOAL>ProbabilityTheory.Kernel.prodMkRight γ (κ + η) = ProbabilityTheory.Kernel.prodMkRight γ κ + ProbabilityTheory.Kernel.prodMkRight γ η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ca : γ × α<VAR>g : β → ℝ≥0∞<GOAL>∫⁻ (b : β), g b ∂(ProbabilityTheory.Kernel.prodMkLeft γ κ) ca = ∫⁻ (b : β), g b ∂κ ca.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ca : α × γ<VAR>g : β → ℝ≥0∞<GOAL>∫⁻ (b : β), g b ∂(ProbabilityTheory.Kernel.prodMkRight γ κ) ca = ∫⁻ (b : β), g b ∂κ ca.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.prodMkLeft Unit κ) ↔ ProbabilityTheory.IsSFiniteKernel κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.prodMkRight Unit κ) ↔ ProbabilityTheory.IsSFiniteKernel κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_6<VAR>MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>f : β → δ<VAR>hf : Measurable f<GOAL>(ProbabilityTheory.Kernel.prodMkLeft γ κ).map f hf = ProbabilityTheory.Kernel.prodMkLeft γ (κ.map f hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>γ : Type u_6<VAR>MeasurableSpace γ<VAR>f : β → δ<VAR>hf : Measurable f<GOAL>(ProbabilityTheory.Kernel.prodMkRight γ κ).map f hf = ProbabilityTheory.Kernel.prodMkRight γ (κ.map f hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel (α × β) γ<VAR>a : β × α<GOAL>κ.swapLeft a = κ a.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel (α × β) γ<VAR>a : β × α<VAR>s : Set γ<GOAL>(κ.swapLeft a) s = (κ a.swap) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel (α × β) γ<VAR>a : β × α<VAR>g : γ → ℝ≥0∞<GOAL>∫⁻ (c : γ), g c ∂κ.swapLeft a = ∫⁻ (c : γ), g c ∂κ a.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>γ : Type u_6<VAR>MeasurableSpace γ<GOAL>(ProbabilityTheory.Kernel.prodMkLeft γ κ).swapLeft = ProbabilityTheory.Kernel.prodMkRight γ κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>γ : Type u_6<VAR>MeasurableSpace γ<GOAL>(ProbabilityTheory.Kernel.prodMkRight γ κ).swapLeft = ProbabilityTheory.Kernel.prodMkLeft γ κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<VAR>a : α<GOAL>κ.swapRight a = MeasureTheory.Measure.map Prod.swap (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<VAR>a : α<VAR>s : Set (γ × β)<VAR>hs : MeasurableSet s<GOAL>(κ.swapRight a) s = (κ a) {p | p.swap ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<VAR>a : α<VAR>g : γ × β → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (c : γ × β), g c ∂κ.swapRight a = ∫⁻ (bc : β × γ), g bc.swap ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<VAR>a : α<GOAL>κ.fst a = MeasureTheory.Measure.map Prod.fst (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(κ.fst a) s = (κ a) {p | p.1 ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<GOAL>ProbabilityTheory.Kernel.fst 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<VAR>a : α<VAR>g : β → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (c : β), g c ∂κ.fst a = ∫⁻ (bc : β × γ), g bc.1 ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>f : β → γ<VAR>g : β → δ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>(κ.map (fun x => (f x, g x)) ⋯).fst = κ.map f hf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>γ : Type u_6<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>hf : Measurable f<GOAL>(κ.map (fun a => (a, f a)) ⋯).fst = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>ProbabilityTheory.IsMarkovKernel η<GOAL>(κ.compProd η).fst = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>δ : Type u_6<VAR>MeasurableSpace δ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<GOAL>(ProbabilityTheory.Kernel.prodMkLeft δ κ).fst = ProbabilityTheory.Kernel.prodMkLeft δ κ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<VAR>δ : Type u_6<VAR>MeasurableSpace δ<GOAL>(ProbabilityTheory.Kernel.prodMkRight δ κ).fst = ProbabilityTheory.Kernel.prodMkRight δ κ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<VAR>a : α<GOAL>κ.snd a = MeasureTheory.Measure.map Prod.snd (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>(κ.snd a) s = (κ a) {p | p.2 ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<GOAL>ProbabilityTheory.Kernel.snd 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<VAR>a : α<VAR>g : γ → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (c : γ), g c ∂κ.snd a = ∫⁻ (bc : β × γ), g bc.2 ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>f : β → γ<VAR>g : β → δ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>(κ.map (fun x => (f x, g x)) ⋯).snd = κ.map g hg
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>γ : Type u_6<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>hf : Measurable f<GOAL>(κ.map (fun a => (f a, a)) ⋯).snd = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>δ : Type u_6<VAR>MeasurableSpace δ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<GOAL>(ProbabilityTheory.Kernel.prodMkLeft δ κ).snd = ProbabilityTheory.Kernel.prodMkLeft δ κ.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<VAR>δ : Type u_6<VAR>MeasurableSpace δ<GOAL>(ProbabilityTheory.Kernel.prodMkRight δ κ).snd = ProbabilityTheory.Kernel.prodMkRight δ κ.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<GOAL>κ.swapRight.fst = κ.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α (β × γ)<GOAL>κ.swapRight.snd = κ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>η : ProbabilityTheory.Kernel β γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>a : α<GOAL>(η.comp κ) a = (κ a).bind ⇑η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>η : ProbabilityTheory.Kernel β γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((η.comp κ) a) s = ∫⁻ (b : β), (η b) s ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>η : ProbabilityTheory.Kernel β γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<GOAL>η.comp κ = (κ.compProd (ProbabilityTheory.Kernel.prodMkLeft α η)).snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>η : ProbabilityTheory.Kernel β γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>a : α<VAR>g : γ → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (c : γ), g c ∂(η.comp κ) a = ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂η b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>ξ : ProbabilityTheory.Kernel γ δ<VAR>ProbabilityTheory.IsSFiniteKernel ξ<VAR>η : ProbabilityTheory.Kernel β γ<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>(ξ.comp η).comp κ = ξ.comp (η.comp κ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>hf : Measurable f<VAR>κ : ProbabilityTheory.Kernel α β<GOAL>(ProbabilityTheory.Kernel.deterministic f hf).comp κ = κ.map f hf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>g : γ → α<VAR>κ : ProbabilityTheory.Kernel α β<VAR>hg : Measurable g<GOAL>κ.comp (ProbabilityTheory.Kernel.deterministic g hg) = κ.comap g hg
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>s : Set (β × γ)<VAR>hs : MeasurableSet s<GOAL>((κ.prod η) a) s = ∫⁻ (b : β), (η a) {c | (b, c) ∈ s} ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<GOAL>(κ.prod η) a = (κ a).prod (η a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>μ : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite μ<VAR>ν : MeasureTheory.Measure γ<VAR>MeasureTheory.SFinite ν<GOAL>(ProbabilityTheory.Kernel.const α μ).prod (ProbabilityTheory.Kernel.const α ν) = ProbabilityTheory.Kernel.const α (μ.prod ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>a : α<VAR>g : β × γ → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (c : β × γ), g c ∂(κ.prod η) a = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsMarkovKernel η<GOAL>(κ.prod η).fst = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsSFiniteKernel η<GOAL>(κ.prod η).snd = η
<VAR>A : Type u_1<VAR>S : Type u_4<VAR>CommRing A<VAR>CommRing S<VAR>M : Submonoid A<VAR>Algebra A S<VAR>IsLocalization M S<VAR>p : A[X]<VAR>r : A<VAR>s : ↥M<VAR>hr : (Polynomial.aeval (IsLocalization.mk' S r s)) p = 0<GOAL>(Polynomial.aeval ((algebraMap A S) r)) (p.scaleRoots ↑s) = 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>p : A[X]<VAR>x : K<VAR>hr : (Polynomial.aeval x) p = 0<GOAL>(p.scaleRoots ↑(IsFractionRing.den A x)).IsRoot (IsFractionRing.num A x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (Polynomial.aeval r) p = 0<GOAL>IsFractionRing.num A r ∣ p.coeff 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (Polynomial.aeval r) p = 0<GOAL>↑(IsFractionRing.den A r) ∣ p.leadingCoeff
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>p : A[X]<VAR>hp : p.Monic<VAR>r : K<VAR>hr : (Polynomial.aeval r) p = 0<GOAL>IsLocalization.IsInteger A r
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>p : A[X]<VAR>hp : p.Monic<VAR>r : K<VAR>hr : (Polynomial.aeval r) p = 0<GOAL>∃ r', r = (algebraMap A K) r' ∧ r' ∣ p.coeff 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<GOAL>IsIntegral A x → IsLocalization.IsInteger A x
<VAR>F : Type u_1<VAR>CommSemiring F<VAR>q : ℕ<VAR>f : Polynomial F<VAR>hf : Polynomial.HasSeparableContraction q f<GOAL>Polynomial.IsSeparableContraction q f hf.contraction
<VAR>F : Type u_1<VAR>CommSemiring F<VAR>q : ℕ<VAR>f : Polynomial F<VAR>hf : Polynomial.HasSeparableContraction q f<VAR>g : Polynomial F<GOAL>Polynomial.IsSeparableContraction q f g → ∃ m, g.natDegree * q ^ m = f.natDegree
<VAR>F : Type u_1<VAR>CommSemiring F<VAR>q : ℕ<VAR>f : Polynomial F<VAR>hf : Polynomial.HasSeparableContraction q f<GOAL>∃ m, hf.degree * q ^ m = f.natDegree
<VAR>F : Type u_1<VAR>CommSemiring F<VAR>q : ℕ<VAR>f : Polynomial F<VAR>hf : Polynomial.HasSeparableContraction q f<GOAL>hf.degree ∣ f.natDegree
<VAR>F : Type u_1<VAR>CommSemiring F<VAR>f : Polynomial F<VAR>hf : Polynomial.HasSeparableContraction 1 f<GOAL>hf.degree = f.natDegree
<VAR>F : Type u_1<VAR>Field F<VAR>q : ℕ<VAR>hF : ExpChar F q<VAR>f : Polynomial F<VAR>irred : Irreducible f<GOAL>Polynomial.HasSeparableContraction q f
<VAR>F : Type u_1<VAR>Field F<VAR>q : ℕ<VAR>hq : NeZero q<VAR>CharP F q<VAR>g g' : Polynomial F<VAR>m m' : ℕ<VAR>h_expand : (Polynomial.expand F (q ^ m)) g = (Polynomial.expand F (q ^ m')) g'<VAR>hg : g.Separable<VAR>hg' : g'.Separable<GOAL>g.natDegree = g'.natDegree
<VAR>F : Type u_1<VAR>Field F<VAR>q : ℕ<VAR>f : Polynomial F<VAR>hf : Polynomial.HasSeparableContraction q f<VAR>hF : ExpChar F q<VAR>g : Polynomial F<VAR>hg : Polynomial.IsSeparableContraction q f g<GOAL>g.natDegree = hf.degree
<VAR>R : Type u_1<VAR>CommRing R<VAR>k : ℕ<VAR>a : R<GOAL>Polynomial.dickson k a 0 = 3 - ↑k
<VAR>R : Type u_1<VAR>CommRing R<VAR>k : ℕ<VAR>a : R<GOAL>Polynomial.dickson k a 1 = Polynomial.X
<VAR>R : Type u_1<VAR>CommRing R<VAR>k : ℕ<VAR>a : R<GOAL>Polynomial.dickson k a 2 = Polynomial.X ^ 2 - Polynomial.C a * (3 - ↑k)
<VAR>R : Type u_1<VAR>CommRing R<VAR>k : ℕ<VAR>a : R<VAR>n : ℕ<GOAL>Polynomial.dickson k a (n + 2) = Polynomial.X * Polynomial.dickson k a (n + 1) - Polynomial.C a * Polynomial.dickson k a n
<VAR>R : Type u_1<VAR>CommRing R<VAR>k : ℕ<VAR>a : R<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>Polynomial.dickson k a n = Polynomial.X * Polynomial.dickson k a (n - 1) - Polynomial.C a * Polynomial.dickson k a (n - 2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>k : ℕ<VAR>a : R<VAR>f : R →+* S<VAR>n : ℕ<GOAL>Polynomial.map f (Polynomial.dickson k a n) = Polynomial.dickson k (f a) n
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<GOAL>Polynomial.dickson 2 0 n = Polynomial.X ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : R<VAR>h : x * y = 1<VAR>n : ℕ<GOAL>Polynomial.eval (x + y) (Polynomial.dickson 1 1 n) = x ^ n + y ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>Invertible 2<GOAL>2 * Polynomial.C ⅟2 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>Invertible 2<GOAL>Polynomial.C ⅟2 * 2 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>Invertible 2<VAR>n : ℕ<GOAL>Polynomial.dickson 1 1 n = 2 * (Polynomial.Chebyshev.T R ↑n).comp (Polynomial.C ⅟2 * Polynomial.X)
<VAR>R : Type u_1<VAR>CommRing R<VAR>Invertible 2<VAR>n : ℕ<GOAL>Polynomial.Chebyshev.T R ↑n = Polynomial.C ⅟2 * (Polynomial.dickson 1 1 n).comp (2 * Polynomial.X)
<VAR>R : Type u_1<VAR>CommRing R<VAR>m n : ℕ<GOAL>Polynomial.dickson 1 1 (m * n) = (Polynomial.dickson 1 1 m).comp (Polynomial.dickson 1 1 n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>m n : ℕ<GOAL>(Polynomial.dickson 1 1 m).comp (Polynomial.dickson 1 1 n) = (Polynomial.dickson 1 1 n).comp (Polynomial.dickson 1 1 m)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>Polynomial.dickson 1 1 p = Polynomial.X ^ p
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP R p<GOAL>Polynomial.dickson 1 1 p = Polynomial.X ^ p
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>r : ℝ<VAR>n : ℕ<VAR>hf : MeasureTheory.Adapted ℱ f<GOAL>MeasureTheory.IsStoppingTime ℱ (MeasureTheory.leastGE f r n)
<VAR>Ω : Type u_1<VAR>f : ℕ → Ω → ℝ<VAR>i : ℕ<VAR>r : ℝ<VAR>ω : Ω<GOAL>MeasureTheory.leastGE f r i ω ≤ i
<VAR>Ω : Type u_1<VAR>f : ℕ → Ω → ℝ<VAR>n m : ℕ<VAR>hnm : n ≤ m<VAR>r : ℝ<VAR>ω : Ω<GOAL>MeasureTheory.leastGE f r n ω ≤ MeasureTheory.leastGE f r m ω
<VAR>Ω : Type u_1<VAR>f : ℕ → Ω → ℝ<VAR>π : Ω → ℕ<VAR>r : ℝ<VAR>ω : Ω<VAR>n : ℕ<VAR>hπn : ∀ (ω : Ω), π ω ≤ n<GOAL>MeasureTheory.leastGE f r (π ω) ω = min (π ω) (MeasureTheory.leastGE f r n ω)
<VAR>Ω : Type u_1<VAR>f : ℕ → Ω → ℝ<VAR>π : Ω → ℕ<VAR>r : ℝ<VAR>n : ℕ<VAR>hπn : ∀ (ω : Ω), π ω ≤ n<GOAL>MeasureTheory.stoppedValue (fun i => MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i)) π = MeasureTheory.stoppedValue (MeasureTheory.stoppedProcess f (MeasureTheory.leastGE f r n)) π
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>r : ℝ<GOAL>MeasureTheory.Submartingale (fun i => MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i)) ℱ μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : ℕ → Ω → ℝ<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>hr : 0 ≤ r<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>i : ℕ<GOAL>∀ᵐ (ω : Ω) ∂μ, MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i) ω ≤ r + ↑R
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hr : 0 ≤ r<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>i : ℕ<GOAL>MeasureTheory.eLpNorm (MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i)) 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal (r + ↑R)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hr : 0 ≤ r<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>i : ℕ<GOAL>MeasureTheory.eLpNorm (MeasureTheory.stoppedValue f (MeasureTheory.leastGE f r i)) 1 μ ≤ ↑(2 * μ Set.univ * ENNReal.ofReal (r + ↑R)).toNNReal
<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>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) → ∃ 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>f : ℕ → Ω → ℝ<VAR>R : ℝ≥0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ 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>f : ℕ → Ω → ℝ<VAR>R : ℝ≥0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ 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>f : ℕ → Ω → ℝ<VAR>R : ℝ≥0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Martingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
<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.Martingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, ¬Filter.Tendsto (fun n => f n ω) Filter.atTop Filter.atTop
<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.Martingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, ¬Filter.Tendsto (fun n => f n ω) Filter.atTop Filter.atBot
<VAR>Ω : Type u_1<VAR>s : ℕ → Set Ω<GOAL>MeasureTheory.BorelCantelli.process s 0 = 0