ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>p : α × β<GOAL>Filter.Tendsto (↑(f p)) Filter.atBot (𝓝 0)
<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>x : ℝ<GOAL>Measurable fun p => ↑(f p) x
<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>s : Set β<VAR>_hs : MeasurableSet s<VAR>x : ℝ<GOAL>∫ (b : β) in s, ↑(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>f : α × β → StieltjesFunction<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>self : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>p : α × β<GOAL>Filter.Tendsto (↑(f p)) 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 : α × β → StieltjesFunction<VAR>hf : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>p : α × β<VAR>x : ℝ<GOAL>0 ≤ ↑(f p) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>hf : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>p : α × β<VAR>x : ℝ<GOAL>↑(f p) x ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>hf : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<GOAL>∫ (b : β), ↑(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>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>f : α × β → StieltjesFunction<VAR>hf : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>x : ℝ<GOAL>∫⁻ (b : β) in s, ENNReal.ofReal (↑(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>ProbabilityTheory.IsFiniteKernel κ<VAR>f : α × β → StieltjesFunction<VAR>hf : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<GOAL>∫⁻ (b : β), ENNReal.ofReal (↑(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>hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν<VAR>ProbabilityTheory.IsFiniteKernel κ<GOAL>ProbabilityTheory.IsCondKernelCDF (ProbabilityTheory.stieltjesOfMeasurableRat f ⋯) κ ν
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>f : α → StieltjesFunction<VAR>hf : ∀ (q : ℝ), Measurable fun a => ↑(f a) q<VAR>hf_bot : ∀ (a : α), Filter.Tendsto (↑(f a)) Filter.atBot (𝓝 0)<VAR>hf_top : ∀ (a : α), Filter.Tendsto (↑(f a)) Filter.atTop (𝓝 1)<GOAL>Measurable fun a => (f a).measure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<GOAL>∀ {x : MeasurableSpace β} {f : α × β → StieltjesFunction} {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {hf : ProbabilityTheory.IsCondKernelCDF f κ ν} (p : α × β), (ProbabilityTheory.IsCondKernelCDF.toKernel f hf) p = (f p).measure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<GOAL>∀ {x : MeasurableSpace β} {f : α × β → StieltjesFunction} {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {hf : ProbabilityTheory.IsCondKernelCDF f κ ν} (p : α × β) (x_1 : ℝ), ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) p) (Set.Iic x_1) = ENNReal.ofReal (↑(f p) x_1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) (Set.Iic 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 : α × β → StieltjesFunction<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) Set.univ ∂ν a = (κ a) (s ×ˢ Set.univ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>a : α<GOAL>∫⁻ (b : β), ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) Set.univ ∂ν a = (κ a) Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set ℝ<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf : ProbabilityTheory.IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set (β × ℝ)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β), ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ s} ∂ν a = (κ a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α (β × ℝ)<VAR>ν : ProbabilityTheory.Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsSFiniteKernel ν<VAR>hf : ProbabilityTheory.IsCondKernelCDF f κ ν<GOAL>ν ⊗ₖ ProbabilityTheory.IsCondKernelCDF.toKernel f hf = κ
<VAR>α β : Type u<VAR>f : α → β<VAR>p : PMF α<GOAL>f <$> p = PMF.map f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : PMF α<VAR>b : β<GOAL>(PMF.map f p) b = ∑' (a : α), if b = f a then p a else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : PMF α<GOAL>(PMF.map f p).support = f '' p.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : PMF α<VAR>b : β<GOAL>b ∈ (PMF.map f p).support ↔ ∃ a ∈ p.support, f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : PMF α<GOAL>p.bind (PMF.pure ∘ f) = PMF.map f p
<VAR>α : Type u_1<VAR>p : PMF α<GOAL>PMF.map id p = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>p : PMF α<VAR>g : β → γ<GOAL>PMF.map g (PMF.map f p) = PMF.map (g ∘ f) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<GOAL>PMF.map f (PMF.pure a) = PMF.pure (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>q : α → PMF β<VAR>f : β → γ<GOAL>PMF.map f (p.bind q) = p.bind fun a => PMF.map f (q a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : α → β<VAR>q : β → PMF γ<GOAL>(PMF.map f p).bind q = p.bind (q ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : PMF α<VAR>b : β<GOAL>PMF.map (Function.const α b) p = PMF.pure b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : PMF α<VAR>s : Set β<GOAL>(PMF.map f p).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : PMF α<VAR>s : Set β<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>hf : Measurable f<VAR>hs : MeasurableSet s<GOAL>(PMF.map f p).toMeasure s = p.toMeasure (f ⁻¹' s)
<VAR>α β : Type u<VAR>q : PMF (α → β)<VAR>p : PMF α<GOAL>(Seq.seq q fun x => p) = q.seq p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : PMF (α → β)<VAR>p : PMF α<VAR>b : β<GOAL>(q.seq p) b = ∑' (f : α → β) (a : α), if b = f a then q f * p a else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : PMF (α → β)<VAR>p : PMF α<GOAL>(q.seq p).support = ⋃ f ∈ q.support, f '' p.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : PMF (α → β)<VAR>p : PMF α<VAR>b : β<GOAL>b ∈ (q.seq p).support ↔ ∃ f ∈ q.support, b ∈ f '' p.support
<VAR>α : Type u_1<VAR>f : α → ENNReal<VAR>s : Finset α<VAR>h : ∑ a ∈ s, f a = 1<VAR>h' : ∀ a ∉ s, f a = 0<VAR>a : α<GOAL>(PMF.ofFinset f s h h') a = f a
<VAR>α : Type u_1<VAR>f : α → ENNReal<VAR>s : Finset α<VAR>h : ∑ a ∈ s, f a = 1<VAR>h' : ∀ a ∉ s, f a = 0<GOAL>(PMF.ofFinset f s h h').support = ↑s ∩ Function.support f
<VAR>α : Type u_1<VAR>f : α → ENNReal<VAR>s : Finset α<VAR>h : ∑ a ∈ s, f a = 1<VAR>h' : ∀ a ∉ s, f a = 0<VAR>a : α<GOAL>a ∈ (PMF.ofFinset f s h h').support ↔ a ∈ s ∧ f a ≠ 0
<VAR>α : Type u_1<VAR>f : α → ENNReal<VAR>s : Finset α<VAR>h : ∑ a ∈ s, f a = 1<VAR>h' : ∀ a ∉ s, f a = 0<VAR>a : α<VAR>ha : a ∉ s<GOAL>(PMF.ofFinset f s h h') a = 0
<VAR>α : Type u_1<VAR>f : α → ENNReal<VAR>s : Finset α<VAR>h : ∑ a ∈ s, f a = 1<VAR>h' : ∀ a ∉ s, f a = 0<VAR>t : Set α<GOAL>(PMF.ofFinset f s h h').toOuterMeasure t = ∑' (x : α), t.indicator f x
<VAR>α : Type u_1<VAR>f : α → ENNReal<VAR>s : Finset α<VAR>h : ∑ a ∈ s, f a = 1<VAR>h' : ∀ a ∉ s, f a = 0<VAR>t : Set α<VAR>MeasurableSpace α<VAR>ht : MeasurableSet t<GOAL>(PMF.ofFinset f s h h').toMeasure t = ∑' (x : α), t.indicator f x
<VAR>α : Type u_1<VAR>Fintype α<VAR>f : α → ENNReal<VAR>h : ∑ a : α, f a = 1<VAR>a : α<GOAL>(PMF.ofFintype f h) a = f a
<VAR>α : Type u_1<VAR>Fintype α<VAR>f : α → ENNReal<VAR>h : ∑ a : α, f a = 1<GOAL>(PMF.ofFintype f h).support = Function.support f
<VAR>α : Type u_1<VAR>Fintype α<VAR>f : α → ENNReal<VAR>h : ∑ a : α, f a = 1<VAR>a : α<GOAL>a ∈ (PMF.ofFintype f h).support ↔ f a ≠ 0
<VAR>α : Type u_1<VAR>Fintype α<VAR>f : α → ENNReal<VAR>h : ∑ a : α, f a = 1<VAR>s : Set α<GOAL>(PMF.ofFintype f h).toOuterMeasure s = ∑' (x : α), s.indicator f x
<VAR>α : Type u_1<VAR>Fintype α<VAR>f : α → ENNReal<VAR>h : ∑ a : α, f a = 1<VAR>s : Set α<VAR>MeasurableSpace α<VAR>hs : MeasurableSet s<GOAL>(PMF.ofFintype f h).toMeasure s = ∑' (x : α), s.indicator f x
<VAR>α : Type u_1<VAR>f : α → ENNReal<VAR>hf0 : tsum f ≠ 0<VAR>hf : tsum f ≠ ⊤<VAR>a : α<GOAL>(PMF.normalize f hf0 hf) a = f a * (∑' (x : α), f x)⁻¹
<VAR>α : Type u_1<VAR>f : α → ENNReal<VAR>hf0 : tsum f ≠ 0<VAR>hf : tsum f ≠ ⊤<GOAL>(PMF.normalize f hf0 hf).support = Function.support f
<VAR>α : Type u_1<VAR>f : α → ENNReal<VAR>hf0 : tsum f ≠ 0<VAR>hf : tsum f ≠ ⊤<VAR>a : α<GOAL>a ∈ (PMF.normalize f hf0 hf).support ↔ f a ≠ 0
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<VAR>h : ∃ a ∈ s, a ∈ p.support<VAR>a : α<GOAL>(p.filter s h) a = s.indicator (⇑p) a * (∑' (a' : α), s.indicator (⇑p) a')⁻¹
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<VAR>h : ∃ a ∈ s, a ∈ p.support<VAR>a : α<VAR>ha : a ∉ s<GOAL>(p.filter s h) a = 0
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<VAR>h : ∃ a ∈ s, a ∈ p.support<VAR>a : α<GOAL>a ∈ (p.filter s h).support ↔ a ∈ s ∧ a ∈ p.support
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<VAR>h : ∃ a ∈ s, a ∈ p.support<GOAL>(p.filter s h).support = s ∩ p.support
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<VAR>h : ∃ a ∈ s, a ∈ p.support<VAR>a : α<GOAL>(p.filter s h) a = 0 ↔ a ∉ s ∨ a ∉ p.support
<VAR>α : Type u_1<VAR>p : PMF α<VAR>s : Set α<VAR>h : ∃ a ∈ s, a ∈ p.support<VAR>a : α<GOAL>(p.filter s h) a ≠ 0 ↔ a ∈ s ∧ a ∈ p.support
<VAR>p : ENNReal<VAR>h : p ≤ 1<VAR>b : Bool<GOAL>(PMF.bernoulli p h) b = bif b then p else 1 - p
<VAR>p : ENNReal<VAR>h : p ≤ 1<GOAL>(PMF.bernoulli p h).support = {b | bif b then p ≠ 0 else p ≠ 1}
<VAR>p : ENNReal<VAR>h : p ≤ 1<VAR>b : Bool<GOAL>b ∈ (PMF.bernoulli p h).support ↔ bif b then p ≠ 0 else p ≠ 1
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>x : E<GOAL>MeasureTheory.Martingale (fun x_1 x_2 => x) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>OrderBot ι<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : Ω → E<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hfint : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Martingale (fun x => f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>μ : MeasureTheory.Measure Ω<GOAL>MeasureTheory.Martingale 0 ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>hf : MeasureTheory.Martingale f ℱ μ<GOAL>MeasureTheory.Adapted ℱ f
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>hf : MeasureTheory.Martingale f ℱ μ<VAR>i : ι<GOAL>MeasureTheory.StronglyMeasurable (f i)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>hf : MeasureTheory.Martingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>μ[f j|↑ℱ i] =ᵐ[μ] f i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>hf : MeasureTheory.Martingale f ℱ μ<VAR>i : ι<GOAL>MeasureTheory.Integrable (f i) μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>hf : MeasureTheory.Martingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f j ω ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>hf : MeasureTheory.Martingale f ℱ μ<VAR>hg : MeasureTheory.Martingale g ℱ μ<GOAL>MeasureTheory.Martingale (f + g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>hf : MeasureTheory.Martingale f ℱ μ<GOAL>MeasureTheory.Martingale (-f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>hf : MeasureTheory.Martingale f ℱ μ<VAR>hg : MeasureTheory.Martingale g ℱ μ<GOAL>MeasureTheory.Martingale (f - g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>c : ℝ<VAR>hf : MeasureTheory.Martingale f ℱ μ<GOAL>MeasureTheory.Martingale (c • f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>Preorder E<VAR>hf : MeasureTheory.Martingale f ℱ μ<GOAL>MeasureTheory.Supermartingale f ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>Preorder E<VAR>hf : MeasureTheory.Martingale f ℱ μ<GOAL>MeasureTheory.Submartingale f ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>PartialOrder E<GOAL>MeasureTheory.Martingale f ℱ μ ↔ MeasureTheory.Supermartingale f ℱ μ ∧ MeasureTheory.Submartingale f ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<GOAL>MeasureTheory.Martingale (fun i => μ[f|↑ℱ i]) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>LE E<VAR>hf : MeasureTheory.Supermartingale f ℱ μ<GOAL>MeasureTheory.Adapted ℱ f
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>LE E<VAR>hf : MeasureTheory.Supermartingale f ℱ μ<VAR>i : ι<GOAL>MeasureTheory.StronglyMeasurable (f i)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>LE E<VAR>hf : MeasureTheory.Supermartingale f ℱ μ<VAR>i : ι<GOAL>MeasureTheory.Integrable (f i) μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>LE E<VAR>hf : MeasureTheory.Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>μ[f j|↑ℱ i] ≤ᵐ[μ] f i
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>MeasureTheory.SigmaFiniteFiltration μ ℱ<VAR>f : ι → Ω → ℝ<VAR>hf : MeasureTheory.Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∫ (ω : Ω) in s, f j ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>Preorder E<VAR>CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : MeasureTheory.Supermartingale f ℱ μ<VAR>hg : MeasureTheory.Supermartingale g ℱ μ<GOAL>MeasureTheory.Supermartingale (f + g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>Preorder E<VAR>CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : MeasureTheory.Supermartingale f ℱ μ<VAR>hg : MeasureTheory.Martingale g ℱ μ<GOAL>MeasureTheory.Supermartingale (f + g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>Preorder E<VAR>CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : MeasureTheory.Supermartingale f ℱ μ<GOAL>MeasureTheory.Submartingale (-f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>LE E<VAR>hf : MeasureTheory.Submartingale f ℱ μ<GOAL>MeasureTheory.Adapted ℱ f
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>LE E<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>i : ι<GOAL>MeasureTheory.StronglyMeasurable (f i)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>LE E<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>i : ι<GOAL>MeasureTheory.Integrable (f i) μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>LE E<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>f i ≤ᵐ[μ] μ[f j|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>Preorder E<VAR>CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hg : MeasureTheory.Submartingale g ℱ μ<GOAL>MeasureTheory.Submartingale (f + g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>Preorder E<VAR>CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hg : MeasureTheory.Martingale g ℱ μ<GOAL>MeasureTheory.Submartingale (f + g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ι → Ω → E<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>Preorder E<VAR>CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : MeasureTheory.Submartingale f ℱ μ<GOAL>MeasureTheory.Supermartingale (-f) ℱ μ