ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
∃ L', (∀ (k : K), Turing.ListBlank.map (Turing.proj k) L' = Turing.ListBlank.mk (List.map some (S' k)).reverse) ∧ Turing.TM1.stepAux (Turing.TM2to1.trStAct q o) v ((Turing.Tape.move Turing.Dir.right)^[(S k).length] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L))) = Turing.TM1.stepAux q v' ((Turing.Tape.move Turing.Dir.right)^[(S' k).length] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L')))
<VAR>K : Type u_1<VAR>DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>M : Λ → Turing.TM2.Stmt Γ Λ σ<VAR>k : K<VAR>o : Turing.TM2to1.StAct k<VAR>q : Turing.TM2.Stmt Γ Λ σ<VAR>v : σ<VAR>S : List (Γ k)<VAR>L : Turing.ListBlank ((k : K) → Option (Γ k))<VAR>hL : Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some S).reverse<VAR>n : ℕ<VAR>H : n ≤ S.length<GOAL>Turing.Reaches₀ (Turing.TM1.step (Turing.TM2to1.tr M)) { l := some (Turing.TM2to1.Λ'.go k o q), var := v, Tape := Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L) } { l := some (Turing.TM2to1.Λ'.go k o q), var := v, Tape := (Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L)) }
<VAR>K : Type u_1<VAR>DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>M : Λ → Turing.TM2.Stmt Γ Λ σ<VAR>q : Turing.TM2.Stmt Γ Λ σ<VAR>v : σ<VAR>L : Turing.ListBlank ((k : K) → Option (Γ k))<VAR>n : ℕ<GOAL>Turing.Reaches₀ (Turing.TM1.step (Turing.TM2to1.tr M)) { l := some (Turing.TM2to1.Λ'.ret q), var := v, Tape := (Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L)) } { l := some (Turing.TM2to1.Λ'.ret q), var := v, Tape := Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L) }
<VAR>K : Type u_1<VAR>DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>M : Λ → Turing.TM2.Stmt Γ Λ σ<VAR>q : Turing.TM2.Stmt Γ Λ σ<VAR>v : σ<VAR>T : Turing.ListBlank ((i : K) → Option (Γ i))<VAR>k : K<VAR>S : (k : K) → List (Γ k)<VAR>hT : ∀ (k : K), Turing.ListBlank.map (Turing.proj k) T = Turing.ListBlank.mk (List.map some (S k)).reverse<VAR>o : Turing.TM2to1.StAct k<VAR>IH : ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : Turing.ListBlank ((k : K) → Option (Γ k))}, (∀ (k : K), Turing.ListBlank.map (Turing.proj k) T = Turing.ListBlank.mk (List.map some (S k)).reverse) → ∃ b, Turing.TM2to1.TrCfg (Turing.TM2.stepAux q v S) b ∧ Turing.Reaches (Turing.TM1.step (Turing.TM2to1.tr M)) (Turing.TM1.stepAux (Turing.TM2to1.trNormal q) v (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom T))) b<GOAL>∃ b, Turing.TM2to1.TrCfg (Turing.TM2.stepAux (Turing.TM2to1.stRun o q) v S) b ∧ Turing.Reaches (Turing.TM1.step (Turing.TM2to1.tr M)) (Turing.TM1.stepAux (Turing.TM2to1.trNormal (Turing.TM2to1.stRun o q)) v (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom T))) b
<VAR>K : Type u_1<VAR>DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>σ : Type u_4<VAR>M : Λ → Turing.TM2.Stmt Γ Λ σ<GOAL>Turing.Respects (Turing.TM2.step M) (Turing.TM1.step (Turing.TM2to1.tr M)) Turing.TM2to1.TrCfg
<VAR>K : Type u_1<VAR>DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>Inhabited Λ<VAR>σ : Type u_4<VAR>Inhabited σ<VAR>k : K<VAR>L : List (Γ k)<GOAL>Turing.TM2to1.TrCfg (Turing.TM2.init k L) (Turing.TM1.init (Turing.TM2to1.trInit k L))
<VAR>K : Type u_1<VAR>DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>Inhabited Λ<VAR>σ : Type u_4<VAR>Inhabited σ<VAR>M : Λ → Turing.TM2.Stmt Γ Λ σ<VAR>k : K<VAR>L : List (Γ k)<GOAL>(Turing.TM1.eval (Turing.TM2to1.tr M) (Turing.TM2to1.trInit k L)).Dom ↔ (Turing.TM2.eval M k L).Dom
<VAR>K : Type u_1<VAR>DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>Inhabited Λ<VAR>σ : Type u_4<VAR>Inhabited σ<VAR>M : Λ → Turing.TM2.Stmt Γ Λ σ<VAR>k : K<VAR>L : List (Γ k)<VAR>L₁ : Turing.ListBlank Turing.TM2to1.Γ'<VAR>L₂ : List (Γ k)<VAR>H₁ : L₁ ∈ Turing.TM1.eval (Turing.TM2to1.tr M) (Turing.TM2to1.trInit k L)<VAR>H₂ : L₂ ∈ Turing.TM2.eval M k L<GOAL>∃ S L', Turing.TM2to1.addBottom L' = L₁ ∧ (∀ (k : K), Turing.ListBlank.map (Turing.proj k) L' = Turing.ListBlank.mk (List.map some (S k)).reverse) ∧ S k = L₂
<VAR>K : Type u_1<VAR>DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>Inhabited Λ<VAR>σ : Type u_4<VAR>M : Λ → Turing.TM2.Stmt Γ Λ σ<VAR>S : Finset Λ<VAR>ss : Turing.TM2.Supports M S<GOAL>Turing.TM1.Supports (Turing.TM2to1.tr M) (Turing.TM2to1.trSupp M S)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>InfSet ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n m : ι<GOAL>MeasureTheory.hitting u s n m = fun x => if ∃ j ∈ Set.Icc n m, u j x ∈ s then sInf (Set.Icc n m ∩ {i | u i x ∈ s}) else m
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n : ι<VAR>ω : Ω<VAR>m : ι<VAR>h : m < n<GOAL>MeasureTheory.hitting u s n m ω = m
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n m : ι<VAR>ω : Ω<GOAL>MeasureTheory.hitting u s n m ω ≤ m
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n : ι<VAR>ω : Ω<VAR>m k : ι<VAR>hk₁ : k < MeasureTheory.hitting u s n m ω<VAR>hk₂ : n ≤ k<GOAL>u k ω ∉ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n : ι<VAR>ω : Ω<VAR>m : ι<GOAL>MeasureTheory.hitting u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) = m
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n : ι<VAR>ω : Ω<VAR>m : ι<VAR>hmn : m ≤ n<GOAL>MeasureTheory.hitting u s n m ω = m
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n m : ι<VAR>hnm : n ≤ m<VAR>ω : Ω<GOAL>n ≤ MeasureTheory.hitting u s n m ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n : ι<VAR>ω : Ω<VAR>m : ι<VAR>h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s<GOAL>n ≤ MeasureTheory.hitting u s n m ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n m : ι<VAR>hnm : n ≤ m<VAR>ω : Ω<GOAL>MeasureTheory.hitting u s n m ω ∈ Set.Icc n m
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n : ι<VAR>ω : Ω<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>m : ι<VAR>h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s<GOAL>u (MeasureTheory.hitting u s n m ω) ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n : ι<VAR>ω : Ω<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>m : ι<VAR>hl : MeasureTheory.hitting u s n m ω < m<GOAL>u (MeasureTheory.hitting u s n m ω) ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>hin : n ≤ i<VAR>him : i ≤ m<VAR>his : u i ω ∈ s<GOAL>MeasureTheory.hitting u s n m ω ≤ i
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>m : ι<VAR>h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s<GOAL>MeasureTheory.hitting u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n : ι<VAR>ω : Ω<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>m : ι<VAR>i : ι<VAR>hi : i < m<GOAL>MeasureTheory.hitting u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n : ι<VAR>ω : Ω<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>m : ι<VAR>i : ι<VAR>hi : i ≤ m<GOAL>MeasureTheory.hitting u s n m ω < i ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n : ι<VAR>ω : Ω<VAR>m₁ m₂ : ι<VAR>h : m₁ ≤ m₂<VAR>h' : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s<GOAL>MeasureTheory.hitting u s n m₁ ω = MeasureTheory.hitting u s n m₂ ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n : ι<VAR>ω : Ω<VAR>m₁ m₂ : ι<VAR>hm : m₁ ≤ m₂<GOAL>MeasureTheory.hitting u s n m₁ ω ≤ MeasureTheory.hitting u s n m₂ ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>ConditionallyCompleteLinearOrder ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>Countable ι<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>f : MeasureTheory.Filtration ι m<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n n' : ι<VAR>hu : MeasureTheory.Adapted f u<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.IsStoppingTime f (MeasureTheory.hitting u s n n')
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrder ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n m : ι<VAR>ω : Ω<VAR>h : ∃ j ∈ Set.Icc n m, u j ω ∈ s<GOAL>MeasureTheory.stoppedValue u (MeasureTheory.hitting u s n m) ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>ConditionallyCompleteLinearOrder ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>Countable ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>f : MeasureTheory.Filtration ι m<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>N : ι<VAR>hτbdd : ∀ (x : Ω), τ x ≤ N<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.Adapted f u<GOAL>MeasureTheory.IsStoppingTime f fun x => MeasureTheory.hitting u s (τ x) N x
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>CompleteLattice ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>ω : Ω<GOAL>MeasureTheory.hitting u s ⊥ ⊤ ω = sInf {i | u i ω ∈ s}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ConditionallyCompleteLinearOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>i n : ι<VAR>ω : Ω<VAR>hx : ∃ j ≤ n, u j ω ∈ s<GOAL>MeasureTheory.hitting u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>m₁ m₂ m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → E<VAR>hle₁ : m₁ ≤ m<VAR>hle₂ : m₂ ≤ m<VAR>MeasureTheory.SigmaFinite (μ.trim hle₂)<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hindp : ProbabilityTheory.Indep m₁ m₂ μ<GOAL>μ[f|m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<VAR>hκs : ∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)<GOAL>Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<GOAL>Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>s : Set (β × γ)<VAR>hs : MeasurableSet s<VAR>a : α<GOAL>Measurable fun b => (η (a, b)) (Prod.mk b ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>s : Set (β × α)<VAR>hs : MeasurableSet s<GOAL>Measurable fun y => (κ y) ((fun x => (x, y)) ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<VAR>c : ℝ≥0∞<GOAL>Measurable fun a => ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<GOAL>Measurable fun a => ∫⁻ (b : β), f a b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun a => ∫⁻ (b : β), f (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>a : α<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun x => ∫⁻ (y : γ), f (x, y) ∂η (a, x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => ∫⁻ (b : β) in s, f a b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : β × α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun y => ∫⁻ (x : β), f (x, y) ∂κ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : β → α → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<GOAL>Measurable fun y => ∫⁻ (x : β), f x y ∂κ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : β → α → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => ∫⁻ (a : β) in s, f a b ∂κ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun a => ∫⁻ (b : β), f b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : β → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => ∫⁻ (b : β) in s, f b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : α → β → E<VAR>hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)<GOAL>MeasurableSet {x | MeasureTheory.Integrable (f x) (κ x)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : α → β → E<VAR>hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)<GOAL>MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f x y ∂κ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : α × β → E<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂κ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>a : α<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>f : β × γ → E<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable fun x => ∫ (y : γ), f (x, y) ∂η (a, x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : β → α → E<VAR>hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)<GOAL>MeasureTheory.StronglyMeasurable fun y => ∫ (x : β), f x y ∂κ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : β × α → E<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable fun y => ∫ (x : β), f (x, y) ∂κ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>η : ProbabilityTheory.Kernel (α × β) γ<VAR>a : α<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>f : γ × β → E<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable fun y => ∫ (x : γ), f (x, y) ∂η (a, y)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>p : PMF α<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f p.toMeasure<GOAL>∫ (a : α), f a ∂p.toMeasure = ∑' (a : α), (p a).toReal • f a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>Fintype α<VAR>p : PMF α<VAR>f : α → E<GOAL>∫ (a : α), f a ∂p.toMeasure = ∑ a : α, (p a).toReal • f a
<VAR>p : ENNReal<VAR>h : p ≤ 1<GOAL>∫ (b : Bool), bif b then 1 else 0 ∂(PMF.bernoulli p h).toMeasure = p.toReal
<VAR>f : ℕ →. ℕ<VAR>hf : Nat.Partrec f<GOAL>Nat.Partrec (Nat.unpaired fun a m => Part.map (fun x => x + m) (Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + m))))
<VAR>n₁ n₂ : ℕ<GOAL>Nat.Partrec.Code.const n₁ = Nat.Partrec.Code.const n₂ → n₁ = n₂
<VAR>n : ℕ<GOAL>(Nat.Partrec.Code.ofNatCode n).encodeCode = n
<GOAL>Encodable.encode = Nat.Partrec.Code.encodeCode
<GOAL>Denumerable.ofNat Nat.Partrec.Code = Nat.Partrec.Code.ofNatCode
<VAR>cf cg : Nat.Partrec.Code<GOAL>Encodable.encode cf < Encodable.encode (cf.pair cg) ∧ Encodable.encode cg < Encodable.encode (cf.pair cg)
<VAR>cf cg : Nat.Partrec.Code<GOAL>Encodable.encode cf < Encodable.encode (cf.comp cg) ∧ Encodable.encode cg < Encodable.encode (cf.comp cg)
<VAR>cf cg : Nat.Partrec.Code<GOAL>Encodable.encode cf < Encodable.encode (cf.prec cg) ∧ Encodable.encode cg < Encodable.encode (cf.prec cg)
<VAR>cf : Nat.Partrec.Code<GOAL>Encodable.encode cf < Encodable.encode cf.rfind'
<GOAL>Primrec₂ Nat.Partrec.Code.pair
<GOAL>Primrec₂ Nat.Partrec.Code.comp
<GOAL>Primrec₂ Nat.Partrec.Code.prec
<GOAL>Primrec Nat.Partrec.Code.rfind'
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>Primcodable α<VAR>Primcodable σ<VAR>c : α → Nat.Partrec.Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ<VAR>hpr : Primrec₂ pr<VAR>co : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ<VAR>hco : Primrec₂ co<VAR>pc : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ<VAR>hpc : Primrec₂ pc<VAR>rf : α → Nat.Partrec.Code × σ → σ<VAR>hrf : Primrec₂ rf<GOAL>let PR := fun a cf cg hf hg => pr a (cf, cg, hf, hg);
let CO := fun a cf cg hf hg => co a (cf, cg, hf, hg);
let PC := fun a cf cg hf hg => pc a (cf, cg, hf, hg);
let F := fun a c => Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a);
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>Primcodable α<VAR>Primcodable σ<VAR>c : α → Nat.Partrec.Code<VAR>hc : Primrec c<VAR>z : α → σ<VAR>hz : Primrec z<VAR>s : α → σ<VAR>hs : Primrec s<VAR>l : α → σ<VAR>hl : Primrec l<VAR>r : α → σ<VAR>hr : Primrec r<VAR>pr : α → Nat.Partrec.Code → Nat.Partrec.Code → σ → σ → σ<VAR>hpr : Primrec fun a => pr a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2<VAR>co : α → Nat.Partrec.Code → Nat.Partrec.Code → σ → σ → σ<VAR>hco : Primrec fun a => co a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2<VAR>pc : α → Nat.Partrec.Code → Nat.Partrec.Code → σ → σ → σ<VAR>hpc : Primrec fun a => pc a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2<VAR>rf : α → Nat.Partrec.Code → σ → σ<VAR>hrf : Primrec fun a => rf a.1 a.2.1 a.2.2<GOAL>let F := fun a c => Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (pr a) (co a) (pc a) (rf a);
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>Primcodable α<VAR>Primcodable σ<VAR>c : α → Nat.Partrec.Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Nat.Partrec.Code × σ → σ<VAR>hrf : Computable₂ rf<GOAL>let PR := fun a cf cg hf hg => pr a (cf, cg, hf, hg);
<VAR>cf cg : Nat.Partrec.Code<VAR>a : ℕ<GOAL>(cf.prec cg).eval (Nat.pair a 0) = cf.eval a
<VAR>cf cg : Nat.Partrec.Code<VAR>a k : ℕ<GOAL>(cf.prec cg).eval (Nat.pair a k.succ) = do let ih ← (cf.prec cg).eval (Nat.pair a k) cg.eval (Nat.pair a (Nat.pair k ih))
<VAR>n m : ℕ<GOAL>(Nat.Partrec.Code.const n).eval m = Part.some n
<VAR>n : ℕ<GOAL>Nat.Partrec.Code.id.eval n = Part.some n
<VAR>c : Nat.Partrec.Code<VAR>n x : ℕ<GOAL>(c.curry n).eval x = c.eval (Nat.pair n x)
<GOAL>Primrec₂ Nat.Partrec.Code.curry
<VAR>c₁ c₂ : Nat.Partrec.Code<VAR>n₁ n₂ : ℕ<VAR>h : c₁.curry n₁ = c₂.curry n₂<GOAL>c₁ = c₂ ∧ n₁ = n₂
<GOAL>∃ f, Computable₂ f ∧ ∀ (c : Nat.Partrec.Code) (n x : ℕ), (f c n).eval x = c.eval (Nat.pair n x)
<VAR>f : ℕ →. ℕ<GOAL>Nat.Partrec f ↔ ∃ c, c.eval = f
<VAR>k : ℕ<VAR>c : Nat.Partrec.Code<VAR>n x : ℕ<GOAL>x ∈ Nat.Partrec.Code.evaln k c n → n < k
<VAR>k₁ k₂ : ℕ<VAR>c : Nat.Partrec.Code<VAR>n x : ℕ<GOAL>k₁ ≤ k₂ → x ∈ Nat.Partrec.Code.evaln k₁ c n → x ∈ Nat.Partrec.Code.evaln k₂ c n
<VAR>k : ℕ<VAR>c : Nat.Partrec.Code<VAR>n x : ℕ<GOAL>x ∈ Nat.Partrec.Code.evaln k c n → x ∈ c.eval n
<VAR>c : Nat.Partrec.Code<VAR>n x : ℕ<GOAL>x ∈ c.eval n ↔ ∃ k, x ∈ Nat.Partrec.Code.evaln k c n
<GOAL>Primrec fun p => Nat.Partrec.Code.lup p.1 p.2.1 p.2.2
<VAR>k : ℕ<VAR>c : Nat.Partrec.Code<VAR>n : ℕ<GOAL>((Option.map (Nat.Partrec.Code.evaln k c) (List.range k)[n]?).bind fun b => b) = Nat.Partrec.Code.evaln k c n
<GOAL>Primrec fun a => Nat.Partrec.Code.evaln a.1.1 a.1.2 a.2
<VAR>c : Nat.Partrec.Code<VAR>n : ℕ<GOAL>c.eval n = Nat.rfindOpt fun k => Nat.Partrec.Code.evaln k c n
<GOAL>Partrec₂ Nat.Partrec.Code.eval
<VAR>f : Nat.Partrec.Code → Nat.Partrec.Code<VAR>hf : Computable f<GOAL>∃ c, (f c).eval = c.eval
<VAR>f : Nat.Partrec.Code → ℕ →. ℕ<VAR>hf : Partrec₂ f<GOAL>∃ c, c.eval = f c
<VAR>α : Type u_1<VAR>p q : PMF α<VAR>h : ∀ (x : α), p x = q x<GOAL>p = q
<VAR>α : Type u_1<VAR>p q : PMF α<GOAL>p = q ↔ ∀ (x : α), p x = q x
<VAR>α : Type u_1<VAR>p : PMF α<GOAL>HasSum (⇑p) 1
<VAR>α : Type u_1<VAR>p : PMF α<GOAL>∑' (a : α), p a = 1
<VAR>α : Type u_1<VAR>p : PMF α<GOAL>∑' (a : α), p a ≠ ⊤
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<GOAL>∑' (a : α), s.indicator (⇑p) a ≠ ⊤
<VAR>α : Type u_1<VAR>p : PMF α<GOAL>⇑p ≠ 0
<VAR>α : Type u_1<VAR>p : PMF α<VAR>a : α<GOAL>a ∈ p.support ↔ p a ≠ 0
<VAR>α : Type u_1<VAR>p : PMF α<GOAL>p.support.Nonempty
<VAR>α : Type u_1<VAR>p : PMF α<GOAL>p.support.Countable
<VAR>α : Type u_1<VAR>p : PMF α<VAR>a : α<GOAL>p a = 0 ↔ a ∉ p.support
<VAR>α : Type u_1<VAR>p : PMF α<VAR>a : α<GOAL>0 < p a ↔ a ∈ p.support
<VAR>α : Type u_1<VAR>p : PMF α<VAR>a : α<GOAL>p a = 1 ↔ p.support = {a}
<VAR>α : Type u_1<VAR>p : PMF α<VAR>a : α<GOAL>p a ≤ 1
<VAR>α : Type u_1<VAR>p : PMF α<VAR>a : α<GOAL>p a ≠ ⊤
<VAR>α : Type u_1<VAR>p : PMF α<VAR>a : α<GOAL>p a < ⊤
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<GOAL>p.toOuterMeasure s = ∑' (x : α), s.indicator (⇑p) x