ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.Submartingale 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>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.Supermartingale 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>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>f g : ι → Ω → ℝ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hg : MeasureTheory.Submartingale g ℱ μ<GOAL>MeasureTheory.Submartingale (f ⊔ g) ℱ μ
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>f : ι → Ω → ℝ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<GOAL>MeasureTheory.Submartingale f⁺ ℱ μ
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ι → Ω → ℝ<VAR>hadp : MeasureTheory.Adapted ℱ f<VAR>hint : ∀ (i : ι), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ<GOAL>MeasureTheory.Submartingale f ℱ μ
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ι → Ω → ℝ<VAR>hadp : MeasureTheory.Adapted ℱ f<VAR>hint : ∀ (i : ι), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (i j : ι), i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i|↑ℱ i]<GOAL>MeasureTheory.Submartingale f ℱ μ
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>f : ι → Ω → ℝ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>0 ≤ᵐ[μ] μ[f j - f i|↑ℱ i]
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ι → Ω → ℝ<GOAL>MeasureTheory.Submartingale f ℱ μ ↔ MeasureTheory.Adapted ℱ f ∧ (∀ (i : ι), MeasureTheory.Integrable (f i) μ) ∧ ∀ (i j : ι), i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i|↑ℱ 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.Submartingale 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>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>F : Type u_4<VAR>NormedLatticeAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : MeasureTheory.Supermartingale f ℱ μ<GOAL>MeasureTheory.Supermartingale (c • f) ℱ μ
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>F : Type u_4<VAR>NormedLatticeAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : c ≤ 0<VAR>hf : MeasureTheory.Supermartingale f ℱ μ<GOAL>MeasureTheory.Submartingale (c • f) ℱ μ
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>F : Type u_4<VAR>NormedLatticeAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : MeasureTheory.Submartingale f ℱ μ<GOAL>MeasureTheory.Submartingale (c • f) ℱ μ
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ι m0<VAR>F : Type u_4<VAR>NormedLatticeAddCommGroup F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : c ≤ 0<VAR>hf : MeasureTheory.Submartingale f ℱ μ<GOAL>MeasureTheory.Supermartingale (c • f) ℱ μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : MeasureTheory.Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ<GOAL>MeasureTheory.Submartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : MeasureTheory.Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f (i + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ<GOAL>MeasureTheory.Supermartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : MeasureTheory.Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f (i + 1) ω ∂μ<GOAL>MeasureTheory.Martingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : MeasureTheory.Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), f i ≤ᵐ[μ] μ[f (i + 1)|↑𝒢 i]<GOAL>MeasureTheory.Submartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : MeasureTheory.Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), μ[f (i + 1)|↑𝒢 i] ≤ᵐ[μ] f i<GOAL>MeasureTheory.Supermartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : MeasureTheory.Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), f i =ᵐ[μ] μ[f (i + 1)|↑𝒢 i]<GOAL>MeasureTheory.Martingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : MeasureTheory.Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), 0 ≤ᵐ[μ] μ[f (i + 1) - f i|↑𝒢 i]<GOAL>MeasureTheory.Submartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : MeasureTheory.Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), 0 ≤ᵐ[μ] μ[f i - f (i + 1)|↑𝒢 i]<GOAL>MeasureTheory.Supermartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : MeasureTheory.Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), μ[f (i + 1) - f i|↑𝒢 i] =ᵐ[μ] 0<GOAL>MeasureTheory.Martingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>Preorder E<VAR>MeasureTheory.SigmaFiniteFiltration μ 𝒢<VAR>f : ℕ → Ω → E<VAR>hfmgle : MeasureTheory.Submartingale f 𝒢 μ<VAR>hfadp : MeasureTheory.Adapted 𝒢 fun n => f (n + 1)<VAR>n : ℕ<GOAL>f 0 ≤ᵐ[μ] f n
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>Preorder E<VAR>MeasureTheory.SigmaFiniteFiltration μ 𝒢<VAR>f : ℕ → Ω → E<VAR>hfmgle : MeasureTheory.Supermartingale f 𝒢 μ<VAR>hfadp : MeasureTheory.Adapted 𝒢 fun n => f (n + 1)<VAR>n : ℕ<GOAL>f n ≤ᵐ[μ] f 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.SigmaFiniteFiltration μ 𝒢<VAR>f : ℕ → Ω → E<VAR>hfmgle : MeasureTheory.Martingale f 𝒢 μ<VAR>hfadp : MeasureTheory.Adapted 𝒢 fun n => f (n + 1)<VAR>n : ℕ<GOAL>f n =ᵐ[μ] f 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>LE E<VAR>f : ℕ → Ω → E<VAR>hf : MeasureTheory.Submartingale f 𝒢 μ<VAR>τ : Ω → ℕ<VAR>hτ : MeasureTheory.IsStoppingTime 𝒢 τ<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), τ ω ≤ N<GOAL>MeasureTheory.Integrable (MeasureTheory.stoppedValue f τ) μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>R : ℝ<VAR>ξ f : ℕ → Ω → ℝ<VAR>hf : MeasureTheory.Submartingale f 𝒢 μ<VAR>hξ : MeasureTheory.Adapted 𝒢 ξ<VAR>hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R<VAR>hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω<GOAL>MeasureTheory.Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>𝒢 : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>R : ℝ<VAR>ξ f : ℕ → Ω → ℝ<VAR>hf : MeasureTheory.Submartingale f 𝒢 μ<VAR>hξ : MeasureTheory.Adapted 𝒢 fun n => ξ (n + 1)<VAR>hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R<VAR>hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω<GOAL>MeasureTheory.Submartingale (fun n => ∑ k ∈ Finset.range n, ξ (k + 1) * (f (k + 1) - f k)) 𝒢 μ
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>r : R<GOAL>(Polynomial.opRingEquiv R) (MulOpposite.op ((Polynomial.monomial n) r)) = (Polynomial.monomial n) (MulOpposite.op r)
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : R<GOAL>(Polynomial.opRingEquiv R) (MulOpposite.op (Polynomial.C a)) = Polynomial.C (MulOpposite.op a)
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(Polynomial.opRingEquiv R) (MulOpposite.op Polynomial.X) = Polynomial.X
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>n : ℕ<GOAL>(Polynomial.opRingEquiv R) (MulOpposite.op (Polynomial.C r * Polynomial.X ^ n)) = Polynomial.C (MulOpposite.op r) * Polynomial.X ^ n
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>r : Rᵐᵒᵖ<GOAL>(Polynomial.opRingEquiv R).symm ((Polynomial.monomial n) r) = MulOpposite.op ((Polynomial.monomial n) (MulOpposite.unop r))
<VAR>R : Type u_1<VAR>Semiring R<VAR>a : Rᵐᵒᵖ<GOAL>(Polynomial.opRingEquiv R).symm (Polynomial.C a) = MulOpposite.op (Polynomial.C (MulOpposite.unop a))
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(Polynomial.opRingEquiv R).symm Polynomial.X = MulOpposite.op Polynomial.X
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : Rᵐᵒᵖ<VAR>n : ℕ<GOAL>(Polynomial.opRingEquiv R).symm (Polynomial.C r * Polynomial.X ^ n) = MulOpposite.op (Polynomial.C (MulOpposite.unop r) * Polynomial.X ^ n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : R[X]ᵐᵒᵖ<VAR>n : ℕ<GOAL>((Polynomial.opRingEquiv R) p).coeff n = MulOpposite.op ((MulOpposite.unop p).coeff n)
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : R[X]ᵐᵒᵖ<GOAL>((Polynomial.opRingEquiv R) p).support = (MulOpposite.unop p).support
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : R[X]ᵐᵒᵖ<GOAL>((Polynomial.opRingEquiv R) p).natDegree = (MulOpposite.unop p).natDegree
<VAR>R : Type u_1<VAR>Semiring R<VAR>p : R[X]ᵐᵒᵖ<GOAL>((Polynomial.opRingEquiv R) p).leadingCoeff = MulOpposite.op (MulOpposite.unop p).leadingCoeff
<VAR>Ω : Type u_1<VAR>f : Ω → ℝ≥0∞<VAR>Mf mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>c : ℝ≥0∞<VAR>T : Set Ω<VAR>h_meas_T : MeasurableSet T<VAR>h_ind : ProbabilityTheory.IndepSets {s | MeasurableSet s} {T} μ<VAR>h_meas_f : Measurable f<GOAL>∫⁻ (ω : Ω), f ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
<VAR>Ω : Type u_1<VAR>f g : Ω → ℝ≥0∞<VAR>Mf Mg mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>hMg : Mg ≤ mΩ<VAR>h_ind : ProbabilityTheory.Indep Mf Mg μ<VAR>h_meas_f : Measurable f<VAR>h_meas_g : Measurable g<GOAL>∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>h_meas_f : Measurable f<VAR>h_meas_g : Measurable g<VAR>h_indep_fun : ProbabilityTheory.IndepFun f g μ<GOAL>∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>h_meas_f : AEMeasurable f μ<VAR>h_meas_g : AEMeasurable g μ<VAR>h_indep_fun : ProbabilityTheory.IndepFun f g μ<GOAL>∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>h_meas_f : AEMeasurable f μ<VAR>h_meas_g : AEMeasurable g μ<VAR>h_indep_fun : ProbabilityTheory.IndepFun f g μ<GOAL>∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>X Y : Ω → β<VAR>NormedDivisionRing β<VAR>BorelSpace β<VAR>hXY : ProbabilityTheory.IndepFun X Y μ<VAR>hX : MeasureTheory.Integrable X μ<VAR>hY : MeasureTheory.Integrable Y μ<GOAL>MeasureTheory.Integrable (X * Y) μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>X Y : Ω → β<VAR>NormedDivisionRing β<VAR>BorelSpace β<VAR>hXY : ProbabilityTheory.IndepFun X Y μ<VAR>h'XY : MeasureTheory.Integrable (X * Y) μ<VAR>hX : MeasureTheory.AEStronglyMeasurable X μ<VAR>hY : MeasureTheory.AEStronglyMeasurable Y μ<VAR>h'Y : ¬Y =ᵐ[μ] 0<GOAL>MeasureTheory.Integrable X μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>X Y : Ω → β<VAR>NormedDivisionRing β<VAR>BorelSpace β<VAR>hXY : ProbabilityTheory.IndepFun X Y μ<VAR>h'XY : MeasureTheory.Integrable (X * Y) μ<VAR>hX : MeasureTheory.AEStronglyMeasurable X μ<VAR>hY : MeasureTheory.AEStronglyMeasurable Y μ<VAR>h'X : ¬X =ᵐ[μ] 0<GOAL>MeasureTheory.Integrable Y μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>X Y : Ω → ℝ<VAR>hXY : ProbabilityTheory.IndepFun X Y μ<VAR>hXp : 0 ≤ X<VAR>hYp : 0 ≤ Y<VAR>hXm : AEMeasurable X μ<VAR>hYm : AEMeasurable Y μ<GOAL>MeasureTheory.integral μ (X * Y) = MeasureTheory.integral μ X * MeasureTheory.integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>X Y : Ω → ℝ<VAR>hXY : ProbabilityTheory.IndepFun X Y μ<VAR>hX : MeasureTheory.Integrable X μ<VAR>hY : MeasureTheory.Integrable Y μ<GOAL>MeasureTheory.integral μ (X * Y) = MeasureTheory.integral μ X * MeasureTheory.integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>X Y : Ω → ℝ<VAR>hXY : ProbabilityTheory.IndepFun X Y μ<VAR>hX : MeasureTheory.AEStronglyMeasurable X μ<VAR>hY : MeasureTheory.AEStronglyMeasurable Y μ<GOAL>MeasureTheory.integral μ (X * Y) = MeasureTheory.integral μ X * MeasureTheory.integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>X Y : Ω → ℝ<VAR>hXY : ProbabilityTheory.IndepFun X Y μ<VAR>hX : MeasureTheory.AEStronglyMeasurable X μ<VAR>hY : MeasureTheory.AEStronglyMeasurable Y μ<GOAL>∫ (ω : Ω), X ω * Y ω ∂μ = MeasureTheory.integral μ X * MeasureTheory.integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_2<VAR>β' : Type u_3<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>hfm : Measurable f<VAR>hgm : Measurable g<GOAL>ProbabilityTheory.IndepFun f g μ ↔ ∀ {φ : β → ℝ} {ψ : β' → ℝ}, Measurable φ → Measurable ψ → MeasureTheory.Integrable (φ ∘ f) μ → MeasureTheory.Integrable (ψ ∘ g) μ → MeasureTheory.integral μ (φ ∘ f * ψ ∘ g) = MeasureTheory.integral μ (φ ∘ f) * MeasureTheory.integral μ (ψ ∘ g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>i j : self.J<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (self.f i j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>CategoryTheory.Limits.HasLimits C<VAR>i : D.J<GOAL>OpenEmbedding ⇑(D.ι i).base
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>i j k : D.J<VAR>S : Set ↑↑(D.V (i, j))<GOAL>⇑(CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k)).base '' (⇑(CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).base ⁻¹' S) = ⇑(D.f i k).base ⁻¹' (⇑(D.f i j).base '' S)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>i j k : D.J<VAR>U : TopologicalSpace.Opens ↑↑(D.V (i, j))<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (D.f i j) U ≫ (D.f i k).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f i j)).obj U)) = (CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).c.app (Opposite.op U) ≫ AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k)) (Opposite.unop (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (Opposite.unop (Opposite.op U))))) ≫ (D.V (i, k)).presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>i j k : D.J<VAR>U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.pullback (D.f i j) (D.f i k))<GOAL>∃ (eq : (TopologicalSpace.Opens.map (D.t k i).base).op.obj (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj U)) = Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (CategoryTheory.Limits.pullback.fst (D.f k i) (D.f k j))).obj (Opposite.unop (Opposite.op { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(Opposite.unop (Opposite.op U)), is_open' := ⋯ })))), AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k)) U ≫ (D.t k i).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj U)) ≫ (D.V (k, i)).presheaf.map (CategoryTheory.eqToHom eq) = (D.t' k i j).c.app (Opposite.op U) ≫ AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.fst (D.f k i) (D.f k j)) (Opposite.unop (Opposite.op { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(Opposite.unop (Opposite.op U)), is_open' := ⋯ }))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>i j k : D.J<VAR>U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.pullback (D.f i j) (D.f i k))<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k)) U ≫ (D.t k i).c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))).obj U)) = (D.t' k i j).c.app (Opposite.op U) ≫ AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.fst (D.f k i) (D.f k j)) (Opposite.unop (Opposite.op { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(Opposite.unop (Opposite.op U)), is_open' := ⋯ })) ≫ (D.V (k, i)).presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>CategoryTheory.Limits.HasLimits C<VAR>i j : D.J<VAR>U : TopologicalSpace.Opens ↑↑(D.U i)<GOAL>(TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U) = (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f j i)).obj ((TopologicalSpace.Opens.map (D.t j i).base).obj ((TopologicalSpace.Opens.map (D.f i j).base).obj U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>CategoryTheory.Limits.HasLimits C<VAR>i j k : D.J<VAR>U : TopologicalSpace.Opens ↑↑(D.U i)<GOAL>∃ (eq : Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j k))).obj (Opposite.unop (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).toPrefunctor.1 (Opposite.unop (Opposite.op U)))))) = (TopologicalSpace.Opens.map (D.f j k).base).op.obj (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U)))), D.opensImagePreimageMap i j U ≫ (D.f j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U))) = (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (Opposite.op U) ≫ AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j k)) (Opposite.unop (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).toPrefunctor.1 (Opposite.unop (Opposite.op U))))) ≫ (D.V (j, k)).presheaf.map (CategoryTheory.eqToHom eq)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : AlgebraicGeometry.PresheafedSpace.GlueData C<VAR>CategoryTheory.Limits.HasLimits C<VAR>i j k : D.J<VAR>U : TopologicalSpace.Opens ↑↑(D.U i)<GOAL>D.opensImagePreimageMap i j U ≫ (D.f j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U))) = (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (Opposite.op U) ≫ AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j k)) (Opposite.unop (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).toPrefunctor.1 (Opposite.unop (Opposite.op U))))) ≫ (D.V (j, k)).presheaf.map (CategoryTheory.eqToHom ⋯)