ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>n : ι<VAR>h : MeasureTheory.Martingale f ℱ μ<VAR>hτ : MeasureTheory.IsStoppingTime ℱ τ<VAR>hσ : MeasureTheory.IsStoppingTime ℱ σ<VAR>hσ_le_τ : σ ≤ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>hτ_countable_range : (Set.range τ).Countable<VAR>hσ_countable_range : (Set.range σ).Countable<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<GOAL>MeasureTheory.stoppedValue f σ =ᵐ[μ] μ[MeasureTheory.stoppedValue f τ|hσ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>n : ι<VAR>Countable ι<VAR>h : MeasureTheory.Martingale f ℱ μ<VAR>hτ : MeasureTheory.IsStoppingTime ℱ τ<VAR>hσ : MeasureTheory.IsStoppingTime ℱ σ<VAR>hσ_le_τ : σ ≤ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<GOAL>MeasureTheory.stoppedValue f σ =ᵐ[μ] μ[MeasureTheory.stoppedValue f τ|hσ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrder ι<VAR>OrderBot ι<VAR>TopologicalSpace ι<VAR>DiscreteTopology ι<VAR>MeasurableSpace ι<VAR>BorelSpace ι<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>SecondCountableTopology E<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>n : ι<VAR>h : MeasureTheory.Martingale f ℱ μ<VAR>hτ : MeasureTheory.IsStoppingTime ℱ τ<VAR>hσ : MeasureTheory.IsStoppingTime ℱ σ<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<GOAL>μ[MeasureTheory.stoppedValue f τ|hσ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] MeasureTheory.stoppedValue f τ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrder ι<VAR>OrderBot ι<VAR>TopologicalSpace ι<VAR>DiscreteTopology ι<VAR>MeasurableSpace ι<VAR>BorelSpace ι<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>SecondCountableTopology E<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>h : MeasureTheory.Martingale f ℱ μ<VAR>hτ : MeasureTheory.IsStoppingTime ℱ τ<VAR>hσ : MeasureTheory.IsStoppingTime ℱ σ<VAR>n : ι<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_sf_min : MeasureTheory.SigmaFinite (μ.trim ⋯)<GOAL>(MeasureTheory.stoppedValue f fun x => min (σ x) (τ x)) =ᵐ[μ] μ[MeasureTheory.stoppedValue f τ|hσ.measurableSpace]
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>NormedAddCommGroup β<VAR>BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)<VAR>hfi : ProbabilityTheory.iIndepFun (fun x => mβ) f μ<VAR>hij : i < j<GOAL>ProbabilityTheory.Indep (MeasurableSpace.comap (f j) mβ) (↑(MeasureTheory.Filtration.natural f hf) i) μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>NormedAddCommGroup β<VAR>BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>SecondCountableTopology β<VAR>CompleteSpace β<VAR>NormedSpace ℝ β<VAR>hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)<VAR>hfi : ProbabilityTheory.iIndepFun (fun x => mβ) f μ<VAR>hij : i < j<GOAL>μ[f j|↑(MeasureTheory.Filtration.natural f hf) i] =ᵐ[μ] fun x => ∫ (x : Ω), f j x ∂μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>LinearOrder ι<VAR>i j : ι<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.iIndepSet s μ<VAR>hij : i < j<GOAL>μ[(s j).indicator fun x => 1|↑(MeasureTheory.filtrationOfSet hsm) i] =ᵐ[μ] fun x => (μ (s j)).toReal
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : ProbabilityTheory.iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<GOAL>μ (Filter.limsup s Filter.atTop) = 1
<VAR>p : ENNReal<VAR>h : p ≤ 1<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>(PMF.binomial p h n) i = p ^ ↑i * (1 - p) ^ (↑(Fin.last n) - ↑i) * ↑(n.choose ↑i)
<VAR>p : ENNReal<VAR>h : p ≤ 1<VAR>n : ℕ<GOAL>(PMF.binomial p h n) 0 = (1 - p) ^ n
<VAR>p : ENNReal<VAR>h : p ≤ 1<VAR>n : ℕ<GOAL>(PMF.binomial p h n) (Fin.last n) = p ^ n
<VAR>p : ENNReal<VAR>h : p ≤ 1<VAR>n : ℕ<GOAL>(PMF.binomial p h n) ↑n = p ^ n
<VAR>p : ENNReal<VAR>h : p ≤ 1<GOAL>PMF.binomial p h 1 = PMF.map (fun x => bif x then 1 else 0) (PMF.bernoulli p h)
<VAR>α : Type u_1<VAR>a a' : α<GOAL>(PMF.pure a) a' = if a' = a then 1 else 0
<VAR>α : Type u_1<VAR>a : α<GOAL>(PMF.pure a).support = {a}
<VAR>α : Type u_1<VAR>a a' : α<GOAL>a' ∈ (PMF.pure a).support ↔ a' = a
<VAR>α : Type u_1<VAR>a : α<GOAL>(PMF.pure a) a = 1
<VAR>α : Type u_1<VAR>a a' : α<VAR>h : a' ≠ a<GOAL>(PMF.pure a) a' = 0
<VAR>α : Type u_1<VAR>a : α<VAR>s : Set α<GOAL>(PMF.pure a).toOuterMeasure s = if a ∈ s then 1 else 0
<VAR>α : Type u_1<VAR>a : α<VAR>s : Set α<VAR>MeasurableSpace α<VAR>hs : MeasurableSet s<GOAL>(PMF.pure a).toMeasure s = if a ∈ s then 1 else 0
<VAR>α : Type u_1<VAR>a : α<VAR>MeasurableSpace α<GOAL>(PMF.pure a).toMeasure = MeasureTheory.Measure.dirac a
<VAR>α : Type u_1<VAR>a : α<VAR>MeasurableSpace α<VAR>Countable α<VAR>h : MeasurableSingletonClass α<GOAL>(MeasureTheory.Measure.dirac a).toPMF = PMF.pure a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : α → PMF β<VAR>b : β<GOAL>(p.bind f) b = ∑' (a : α), p a * (f a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : α → PMF β<GOAL>(p.bind f).support = ⋃ a ∈ p.support, (f a).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : α → PMF β<VAR>b : β<GOAL>b ∈ (p.bind f).support ↔ ∃ a ∈ p.support, b ∈ (f a).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>f : α → PMF β<GOAL>(PMF.pure a).bind f = f a
<VAR>α : Type u_1<VAR>p : PMF α<GOAL>p.bind PMF.pure = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>q : PMF β<GOAL>(p.bind fun x => q) = q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : α → PMF β<VAR>g : β → PMF γ<GOAL>(p.bind f).bind g = p.bind fun a => (f a).bind g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>q : PMF β<VAR>f : α → β → PMF γ<GOAL>(p.bind fun a => q.bind (f a)) = q.bind fun b => p.bind fun a => f a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : α → PMF β<VAR>s : Set β<GOAL>(p.bind f).toOuterMeasure s = ∑' (a : α), p a * (f a).toOuterMeasure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : α → PMF β<VAR>s : Set β<VAR>MeasurableSpace β<VAR>hs : MeasurableSet s<GOAL>(p.bind f).toMeasure s = ∑' (a : α), p a * (f a).toMeasure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>b : β<GOAL>(p.bindOnSupport f) b = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<GOAL>(p.bindOnSupport f).support = ⋃ a, ⋃ (h : a ∈ p.support), (f a h).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>b : β<GOAL>b ∈ (p.bindOnSupport f).support ↔ ∃ a, ∃ (h : a ∈ p.support), b ∈ (f a h).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : α → PMF β<GOAL>(p.bindOnSupport fun a x => f a) = p.bind f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>b : β<GOAL>(p.bindOnSupport f) b = 0 ↔ ∀ (a : α) (ha : p a ≠ 0), (f a ha) b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>f : (a' : α) → a' ∈ (PMF.pure a).support → PMF β<GOAL>(PMF.pure a).bindOnSupport f = f a ⋯
<VAR>α : Type u_1<VAR>p : PMF α<GOAL>(p.bindOnSupport fun a x => PMF.pure a) = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ<GOAL>(p.bindOnSupport f).bindOnSupport g = p.bindOnSupport fun a ha => (f a ha).bindOnSupport fun b hb => g b ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>q : PMF β<VAR>f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ<GOAL>(p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) = q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>s : Set β<GOAL>(p.bindOnSupport f).toOuterMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toOuterMeasure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>s : Set β<VAR>MeasurableSpace β<VAR>hs : MeasurableSet s<GOAL>(p.bindOnSupport f).toMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toMeasure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDF f κ ν<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>_hs : MeasurableSet s<VAR>q : ℚ<GOAL>∫ (b : β) in s, f (a, b) q ∂ν a = ((κ a) (s ×ˢ Set.Iic ↑q)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>q : ℚ<GOAL>MeasureTheory.Integrable (fun b => f (a, b) q) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<GOAL>∀ᵐ (b : β) ∂ν a, ProbabilityTheory.IsRatStieltjesPoint f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<GOAL>∀ᵐ (b : β) ∂ν a, Monotone (f (a, b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<GOAL>∀ᵐ (b : β) ∂ν a, Filter.Tendsto (f (a, b)) Filter.atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<GOAL>∀ᵐ (b : β) ∂ν a, Filter.Tendsto (f (a, b)) Filter.atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<GOAL>∀ᵐ (b : β) ∂ν a, ∀ (q : ℚ), ⨅ r, f (a, b) ↑r = f (a, b) q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>q : ℚ<GOAL>(fun b => ↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) =ᵐ[ν a] fun b => f (a, b) q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>q : ℚ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫ (b : β) in s, ↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q ∂ν a = ((κ a) (s ×ˢ Set.Iic ↑q)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>q : ℚ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ENNReal.ofReal (↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) ∂ν a = (κ a) (s ×ˢ Set.Iic ↑q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ENNReal.ofReal (↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = (κ a) (s ×ˢ Set.Iic x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<GOAL>∫⁻ (b : β), ENNReal.ofReal (↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = (κ a) (Set.univ ×ˢ Set.Iic x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<GOAL>MeasureTheory.Integrable (fun b => ↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) x) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫ (b : β) in s, ↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) x ∂ν a = ((κ a) (s ×ˢ Set.Iic x)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<GOAL>∫ (b : β), ↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) x ∂ν a = ((κ a) (Set.univ ×ˢ Set.Iic x)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>q : ℚ<GOAL>∀ᵐ (c : β) ∂ν a, 0 ≤ f (a, c) q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>q : ℚ<GOAL>∀ᵐ (c : β) ∂ν a, f (a, c) q ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>_hs : Monotone seq<VAR>_hs_tendsto : Filter.Tendsto seq Filter.atTop Filter.atTop<GOAL>Filter.Tendsto (fun m => ∫ (c : β), f (a, c) (seq m) ∂ν a) Filter.atTop (𝓝 ((ν a) Set.univ).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>q r : ℚ<VAR>_hqr : q ≤ r<GOAL>∀ᵐ (c : β) ∂ν a, f (a, c) q ≤ f (a, c) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>A : Set β<VAR>_hA : MeasurableSet A<VAR>q : ℚ<GOAL>∫ (c : β) in A, f (a, c) q ∂ν a = ((κ a) (A ×ˢ Set.Iic ↑q)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>_hs : Antitone seq<VAR>_hs_tendsto : Filter.Tendsto seq Filter.atTop Filter.atBot<GOAL>Filter.Tendsto (fun m => ∫ (c : β), f (a, c) (seq m) ∂ν a) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → ℚ → ℝ<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>q : ℚ<GOAL>MeasureTheory.Integrable (fun c => f (a, c) q) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>q : ℚ<GOAL>Measurable fun t => f (a, t) q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<GOAL>∀ᵐ (c : β) ∂ν a, Monotone (f (a, c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<GOAL>∀ᵐ (c : β) ∂ν a, ∀ (q : ℚ), 0 ≤ f (a, c) q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<GOAL>∀ᵐ (c : β) ∂ν a, ∀ (q : ℚ), f (a, c) q ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Antitone seq<VAR>hseq_tendsto : Filter.Tendsto seq Filter.atTop Filter.atBot<GOAL>∀ᵐ (c : β) ∂ν a, Filter.Tendsto (fun m => f (a, c) (seq m)) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Monotone seq<VAR>hseq_tendsto : Filter.Tendsto seq Filter.atTop Filter.atTop<GOAL>∀ᵐ (c : β) ∂ν a, Filter.Tendsto (fun m => f (a, c) (seq m)) Filter.atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, Filter.Tendsto (f (a, t)) Filter.atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, Filter.Tendsto (f (a, t)) Filter.atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, ∀ (q : ℚ), BddBelow (Set.range fun r => f (a, t) ↑r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<GOAL>MeasureTheory.Integrable (fun t => ⨅ r, f (a, t) ↑r) (ν a)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℚ<GOAL>⨅ r, ρ (s ×ˢ Set.Iic ↑↑r) = ρ (s ×ˢ Set.Iic ↑t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<VAR>A : Set β<VAR>hA : MeasurableSet A<GOAL>∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a = ((κ a) (A ×ˢ Set.Iic ↑q)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, ∀ (q : ℚ), ⨅ r, f (a, t) ↑r = f (a, t) q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, ProbabilityTheory.IsRatStieltjesPoint f (a, t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel ν<GOAL>ProbabilityTheory.IsRatCondKernelCDF f κ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α × β → StieltjesFunction<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<GOAL>MeasureTheory.Integrable (fun b => ↑(f (a, b)) x) (ν a)