About
Theorem.market is a platform for sharing and verifying formal proofs using the Lean4 theorem prover.
Solved Theorems
No solved theorems found.
Unsolved Theorems
Fair Games Theorem
Unsolved
By john
13 days ago
Theorem Definition:
theorem MeasureTheory.submartingale_iff_expected_stoppedValue_mono {Ī© : Type u_1} {m0 : MeasurableSpace Ī©} {Ī¼ : Measure Ī©} {š¢ : Filtration ā m0} {f : ā ā Ī© ā ā} [IsFiniteMeasure Ī¼] (hadp : Adapted š¢ f) (hint : ā (i : ā), Integrable (f i) Ī¼) : Submartingale f š¢ Ī¼ ā ā (Ļ Ļ : Ī© ā ā), IsStoppingTime š¢ Ļ ā IsStoppingTime š¢ Ļ ā Ļ ā¤ Ļ ā (ā (N : ā), ā (x : Ī©), Ļ x ā¤ N) ā ā« (x : Ī©), stoppedValue f Ļ x āĪ¼ ā¤ ā« (x : Ī©), stoppedValue f Ļ x āĪ¼ :=
Bezout's Theorem
Unsolved
By john
13 days ago
Theorem Definition:
theorem Nat.gcd_eq_gcd_ab (x y : ā) : ā(x.gcd y) = āx * x.gcdA y + āy * x.gcdB y :=
The Laws of Large Numbers
Unsolved
By john
13 days ago
Theorem Definition:
theorem ProbabilityTheory.strong_law_ae {Ī© : Type u_1} {mĪ© : MeasurableSpace Ī©} {Ī¼ : MeasureTheory.Measure Ī©} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ā E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (X : ā ā Ī© ā E) (hint : MeasureTheory.Integrable (X 0) Ī¼) (hindep : Pairwise (Function.onFun (fun (x1 x2 : Ī© ā E) => IndepFun x1 x2 Ī¼) X)) (hident : ā (i : ā), IdentDistrib (X i) (X 0) Ī¼ Ī¼) : āįµ (Ļ : Ī©) āĪ¼, Filter.Tendsto (fun (n : ā) => (ān)ā»Ā¹ ā¢ ā i ā Finset.range n, X i Ļ) Filter.atTop (nhds (ā« (x : Ī©), X 0 x āĪ¼)) :=
By john
13 days ago
Theorem Definition:
theorem Finset.mem_powersetCard {Ī± : Type u_1} {n : ā} {s t : Finset Ī±} : s ā powersetCard n t ā s ā t ā§ s.card = n :=
By john
13 days ago
Theorem Definition:
theorem Finset.card_powersetCard {Ī± : Type u_1} (n : ā) (s : Finset Ī±) : (powersetCard n s).card = s.card.choose n :=