Add repository information

CODE_OF_CONDUCT.md

@@ -0,0 +1,91 @@
+
+# Contributor Covenant 3.0 Code of Conduct
+
+## Our Pledge
+
+We pledge to make our community welcoming, safe, and equitable for all.
+
+We are committed to fostering an environment that respects and promotes the dignity, rights, and contributions of all individuals, regardless of characteristics including race, ethnicity, caste, color, age, physical characteristics, neurodiversity, disability, sex or gender, gender identity or expression, sexual orientation, language, philosophy or religion, national or social origin, socio-economic position, level of education, or other status. The same privileges of participation are extended to everyone who participates in good faith and in accordance with this Covenant.
+
+## Encouraged Behaviors
+
+While acknowledging differences in social norms, we all strive to meet our community's expectations for positive behavior. We also understand that our words and actions may be interpreted differently than we intend based on culture, background, or native language.
+
+With these considerations in mind, we agree to behave mindfully toward each other and act in ways that center our shared values, including:
+
+1. Respecting the **purpose of our community**, our activities, and our ways of gathering.
+2. Engaging **kindly and honestly** with others.
+3. Respecting **different viewpoints** and experiences.
+4. **Taking responsibility** for our actions and contributions.
+5. Gracefully giving and accepting **constructive feedback**.
+6. Committing to **repairing harm** when it occurs.
+7. Behaving in other ways that promote and sustain the **well-being of our community**.
+
+
+## Restricted Behaviors
+
+We agree to restrict the following behaviors in our community. Instances, threats, and promotion of these behaviors are violations of this Code of Conduct.
+
+1. **Harassment.** Violating explicitly expressed boundaries or engaging in unnecessary personal attention after any clear request to stop.
+2. **Character attacks.** Making insulting, demeaning, or pejorative comments directed at a community member or group of people.
+3. **Stereotyping or discrimination.** Characterizing anyone’s personality or behavior on the basis of immutable identities or traits.
+4. **Sexualization.** Behaving in a way that would generally be considered inappropriately intimate in the context or purpose of the community.
+5. **Violating confidentiality**. Sharing or acting on someone's personal or private information without their permission.
+6. **Endangerment.** Causing, encouraging, or threatening violence or other harm toward any person or group.
+7. Behaving in other ways that **threaten the well-being** of our community.
+
+### Other Restrictions
+
+1. **Misleading identity.** Impersonating someone else for any reason, or pretending to be someone else to evade enforcement actions.
+2. **Failing to credit sources.** Not properly crediting the sources of content you contribute.
+3. **Promotional materials**. Sharing marketing or other commercial content in a way that is outside the norms of the community.
+4. **Irresponsible communication.** Failing to responsibly present content which includes, links or describes any other restricted behaviors.
+
+
+## Reporting an Issue
+
+Tensions can occur between community members even when they are trying their best to collaborate. Not every conflict represents a code of conduct violation, and this Code of Conduct reinforces encouraged behaviors and norms that can help avoid conflicts and minimize harm.
+
+When an incident does occur, it is important to report it promptly. To report a possible violation, **contact one of the project maintainers.**
+
+Community Moderators take reports of violations seriously and will make every effort to respond in a timely manner. They will investigate all reports of code of conduct violations, reviewing messages, logs, and recordings, or interviewing witnesses and other participants. Community Moderators will keep investigation and enforcement actions as transparent as possible while prioritizing safety and confidentiality. In order to honor these values, enforcement actions are carried out in private with the involved parties, but communicating to the whole community may be part of a mutually agreed upon resolution.
+
+
+## Addressing and Repairing Harm
+
+****
+
+If an investigation by the Community Moderators finds that this Code of Conduct has been violated, the following enforcement ladder may be used to determine how best to repair harm, based on the incident's impact on the individuals involved and the community as a whole. Depending on the severity of a violation, lower rungs on the ladder may be skipped.
+
+1) Warning
+   1) Event: A violation involving a single incident or series of incidents.
+   2) Consequence: A private, written warning from the Community Moderators.
+   3) Repair: Examples of repair include a private written apology, acknowledgement of responsibility, and seeking clarification on expectations.
+2) Temporarily Limited Activities
+   1) Event: A repeated incidence of a violation that previously resulted in a warning, or the first incidence of a more serious violation.
+   2) Consequence: A private, written warning with a time-limited cooldown period designed to underscore the seriousness of the situation and give the community members involved time to process the incident. The cooldown period may be limited to particular communication channels or interactions with particular community members.
+   3) Repair: Examples of repair may include making an apology, using the cooldown period to reflect on actions and impact, and being thoughtful about re-entering community spaces after the period is over.
+3) Temporary Suspension
+   1) Event: A pattern of repeated violation which the Community Moderators have tried to address with warnings, or a single serious violation.
+   2) Consequence: A private written warning with conditions for return from suspension. In general, temporary suspensions give the person being suspended time to reflect upon their behavior and possible corrective actions.
+   3) Repair: Examples of repair include respecting the spirit of the suspension, meeting the specified conditions for return, and being thoughtful about how to reintegrate with the community when the suspension is lifted.
+4) Permanent Ban
+   1) Event: A pattern of repeated code of conduct violations that other steps on the ladder have failed to resolve, or a violation so serious that the Community Moderators determine there is no way to keep the community safe with this person as a member.
+   2) Consequence: Access to all community spaces, tools, and communication channels is removed. In general, permanent bans should be rarely used, should have strong reasoning behind them, and should only be resorted to if working through other remedies has failed to change the behavior.
+   3) Repair: There is no possible repair in cases of this severity.
+
+This enforcement ladder is intended as a guideline. It does not limit the ability of Community Managers to use their discretion and judgment, in keeping with the best interests of our community.
+
+
+## Scope
+
+This Code of Conduct applies within all community spaces, and also applies when an individual is officially representing the community in public or other spaces. Examples of representing our community include using an official email address, posting via an official social media account, or acting as an appointed representative at an online or offline event.
+
+
+## Attribution
+
+This Code of Conduct is adapted from the Contributor Covenant, version 3.0, permanently available at [https://www.contributor-covenant.org/version/3/0/](https://www.contributor-covenant.org/version/3/0/).
+
+Contributor Covenant is stewarded by the Organization for Ethical Source and licensed under CC BY-SA 4.0. To view a copy of this license, visit [https://creativecommons.org/licenses/by-sa/4.0/](https://creativecommons.org/licenses/by-sa/4.0/)
+
+For answers to common questions about Contributor Covenant, see the FAQ at [https://www.contributor-covenant.org/faq](https://www.contributor-covenant.org/faq). Translations are provided at [https://www.contributor-covenant.org/translations](https://www.contributor-covenant.org/translations). Additional enforcement and community guideline resources can be found at [https://www.contributor-covenant.org/resources](https://www.contributor-covenant.org/resources). The enforcement ladder was inspired by the work of [Mozilla’s code of conduct team](https://github.com/mozilla/inclusion).

CONTRIBUTING.md

@@ -1,8 +1,27 @@
 # Contributing to Lean Machine Learning
 
-Thank you for your interest in contributing to Lean Machine Learning! We welcome contributions from the community and appreciate your efforts to improve the project. Please follow the guidelines below to ensure a smooth contribution process.
+We welcome contributions from the community and appreciate your efforts to improve the project. Please follow the guidelines below to ensure a smooth contribution process.
 
-[In Construction]
+## How to contribute
+
+Fork the repository and create a new branch for your contribution. Make your changes and submit a pull request to the main branch. Please provide a clear description of your changes and the motivation behind them.
+
+## What to contribute
+
+See the [Roadmap](ROADMAP.md).
+
+#### Finding tasks
+
+Head over to our github issues if you are looking for a short contribution.
+
+## Coordination
+
+Most contributions are welcome as straightforward PRs.
+However, for major developments, it is recommended to discuss it on zulip first.
+
+## Style and documentation
+
+We generally follow the [Mathlib style for coding and documentation](https://leanprover-community.github.io/contribute/style.html), so please read that.
 
 ## Code quality and LLM policy
 

GOVERNANCE.md

@@ -0,0 +1,8 @@
+# Governance model for Lean Machine Learning
+
+The maintainers of LML are responsible for defining the project roadmap and ensuring that contributors can work together in a welcoming environment.
+
+## Maintainers
+
+- Rémy Degenne (@RemyDegenne), Inria centre at the University of Lille
+- Paulo Rauber (@paulorauber), Queen Mary University of London

LeanMachineLearning/BanditAlgorithms/ETC.lean

@@ -203,7 +203,7 @@ lemma probReal_sumRewards_le_sumRewards_le [Nonempty (Fin K)]
   simp_rw [measureReal_def]
   congr 1
   refine measure_congr ?_
-  rw [ae_eq_set_iff]
+  rw [Filter.eventuallyEq_set]
   filter_upwards [pullCount_mul h a, pullCount_mul h (bestArm ν)] with ω ha h_best
   simp [ha, h_best]
 

LeanMachineLearning/ForMathlib/IndepFun.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2025 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne, Paulo Rauber
+-/
 module
 
 public import Mathlib.Probability.IdentDistrib

LeanMachineLearning/ForMathlib/IndepInfinitePi.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2025 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne, Paulo Rauber
+-/
 module
 
 public import Mathlib.Probability.Independence.InfinitePi

LeanMachineLearning/ForMathlib/Measurable.lean

@@ -21,17 +21,10 @@ namespace MeasureTheory
 variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
   {μ : Measure α}
 
-lemma ae_eq_set_iff {s t : Set α} : s =ᵐ[μ] t ↔ ∀ᵐ a ∂μ, a ∈ s ↔ a ∈ t := by
-  rw [Filter.EventuallyEq]
-  simp only [eq_iff_iff]
-  congr!
-
 lemma measurable_comp_comap (f : α → β) {g : β → γ} (hg : Measurable g) :
     Measurable[mβ.comap f] (g ∘ f) := by
   rw [measurable_iff_comap_le, ← MeasurableSpace.comap_comp]
-  refine MeasurableSpace.comap_mono ?_
-  rw [← measurable_iff_comap_le]
-  exact hg
+  exact MeasurableSpace.comap_mono hg.comap_le
 
 @[fun_prop]
 lemma Measurable.coe_nat_enat {f : α → ℕ} (hf : Measurable f) :

LeanMachineLearning/SequentialLearning/FiniteActions.lean

@@ -261,7 +261,6 @@ lemma exists_pullCount_eq (h' : stepsUntil A a m ω ≠ ⊤) :
   rw [← stepsUntil_eq_top_iff] at h_contra
   simp [h_contra] at h'
 
-set_option backward.isDefEq.respectTransparency false in
 lemma stepsUntil_zero_of_ne (hka : A 0 ω ≠ a) : stepsUntil A a 0 ω = 0 := by
   unfold stepsUntil
   simp_rw [← bot_eq_zero, sInf_eq_bot, bot_eq_zero]
@@ -277,7 +276,6 @@ lemma stepsUntil_zero_of_eq (hka : A 0 ω = a) : stepsUntil A a 0 ω = ⊤ := by
   rw [← hka, ← zero_add 1, pullCount_action_eq_pullCount_add_one]
   simp
 
-set_option backward.isDefEq.respectTransparency false in
 lemma stepsUntil_eq_dite (a : α) (m : ℕ) (ω : Ω)
     [Decidable (∃ s, pullCount A a (s + 1) ω = m)] :
     stepsUntil A a m ω =
@@ -337,7 +335,6 @@ lemma stepsUntil_pullCount_le (ω : Ω) (a : α) (t : ℕ) :
   rw [stepsUntil]
   exact csInf_le (OrderBot.bddBelow _) ⟨t, rfl, rfl⟩
 
-set_option backward.isDefEq.respectTransparency false in
 lemma stepsUntil_pullCount_eq (ω : Ω) (t : ℕ) :
     stepsUntil A (A t ω) (pullCount A (A t ω) (t + 1) ω) ω = t := by
   apply le_antisymm (stepsUntil_pullCount_le ω (A t ω) t)
@@ -353,7 +350,6 @@ lemma stepsUntil_one_of_eq (hka : A 0 ω = a) : stepsUntil A a 1 ω = 0 := by
   have h_le := stepsUntil_pullCount_le (A := A) ω a 0
   simpa [h_pull] using h_le
 
-set_option backward.isDefEq.respectTransparency false in
 lemma stepsUntil_eq_zero_iff :
     stepsUntil A a m ω = 0 ↔ (m = 0 ∧ A 0 ω ≠ a) ∨ (m = 1 ∧ A 0 ω = a) := by
   classical
@@ -420,7 +416,6 @@ lemma pullCount_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount A a (s +
   swap; · simpa [stepsUntil_eq_top_iff]
   grind
 
-set_option backward.isDefEq.respectTransparency false in
 lemma pullCount_lt_of_le_stepsUntil (a : α) {n m : ℕ} (ω : Ω)
     (h_exists : ∃ s, pullCount A a (s + 1) ω = m) (hn : n < stepsUntil A a m ω) :
     pullCount A a (n + 1) ω < m := by
@@ -456,7 +451,6 @@ lemma pullCount_add_one_eq_of_stepsUntil_eq_coe {ω : Ω}
   rw [this, pullCount_stepsUntil_add_one]
   exact exists_pullCount_eq (by simp [h])
 
-set_option backward.isDefEq.respectTransparency false in
 lemma stepsUntil_eq_iff {ω : Ω} (n : ℕ) :
     stepsUntil A a m ω = n ↔
       pullCount A a (n + 1) ω = m ∧ (∀ k < n, pullCount A a (k + 1) ω < m) := by
@@ -550,7 +544,6 @@ lemma measurable_stepsUntil' [MeasurableSingletonClass α]
     Measurable (fun ω : Ω × (ℕ → α → R) ↦ stepsUntil A a m ω.1) :=
   (measurable_stepsUntil hA a m).comp measurable_fst
 
-set_option backward.isDefEq.respectTransparency false in
 lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass α]
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) (m n : ℕ) :
     Measurable[MeasurableSpace.comap
@@ -564,8 +557,7 @@ lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass α]
         false_and, or_false]
       refine Measurable.indicator measurable_const ?_
       refine (measurableSet_singleton _).compl.preimage ?_
-      rw [measurable_iff_comap_le]
-      rw [Prod.instMeasurableSpace, MeasurableSpace.comap_prodMk]
+      rw [measurable_iff_comap_le, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMk]
       exact le_sup_of_le_right le_rfl
     · have : {ω | stepsUntil A a 0 ω = n} = ∅ := by
         ext ω
@@ -579,11 +571,9 @@ lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass α]
   simp_rw [stepsUntil_eq_iff' hm]
   refine Measurable.indicator measurable_const ?_
   refine ((measurableSet_singleton _).preimage ?_).inter ((measurableSet_singleton _).preimage ?_)
-  · rw [measurable_iff_comap_le]
-    rw [Prod.instMeasurableSpace, MeasurableSpace.comap_prodMk]
+  · rw [measurable_iff_comap_le, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMk]
     exact le_sup_of_le_right le_rfl
-  · rw [measurable_iff_comap_le]
-    rw [Prod.instMeasurableSpace, MeasurableSpace.comap_prodMk]
+  · rw [measurable_iff_comap_le, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMk]
     refine le_sup_of_le_left ?_
     rw [← measurable_iff_comap_le]
     by_cases hn : n = 0

README.md

@@ -1,18 +1,34 @@
+
+<div align="center">
+
 # Lean Machine Learning
 
-This repository contains a Lean formalization of regret bounds for several stochastic bandit algorithms.
+## The Lean library for machine learning research.
+
+</div>
+
+
+Website: [https://remydegenne.github.io/lean-bandits/](https://remydegenne.github.io/lean-bandits/)
+
+## Goals
 
-Authors: Rémy Degenne, Paulo Rauber.
+- A library of high-quality formalization of machine learning definitions.
+- Essential theorems and proofs in machine learning theory.
+- A framework for working on machine learning algorithms in Lean.
+- An extensive documentation, with examples and tutorials.
+- A trusted basis for formalization of machine learning research.
+
+## Contributing
+
+Please see our [contribution guide](CONTRIBUTING.md) and [code of conduct](CODE_OF_CONDUCT.md).
+
+For discussions, you can reach out to us on the [Lean prover Zulip chat](https://leanprover.zulipchat.com/).
+
+## Current state of the library
+
+As a first proof of concept, the repository contains a formalization of regret bounds for several stochastic bandit algorithms.
 
 Main results:
-- Framework for working on bandit algorithms in Lean.
+- Framework for working on (bandit) algorithms in Lean.
 - Regret bound for the Explore-Then-Commit algorithm.
 - Regret bound for the UCB algorithm.
-
-Contents:
-- Definitions of an iterative, stochastic algorithm and a stochastic environment
-- Proofs of the existence of probability spaces on which those algorithm-environment interactions are defined, and uniqueness of the resulting laws
-- Notations and tools to analyze bandits: number of times an arm was pulled, time of the nth pull, regret, gap. Relations between those.
-- Concentration inequalities
-- Definitions of ETC and UCB
-- Proofs of regret bounds for those two algorithms.

verso/Manual/Front.lean

@@ -15,8 +15,6 @@ authors := ["Rémy Degenne, Paulo Rauber"]
 shortTitle := "Lean Machine Learning"
 %%%
 
-*The Lean Machine Learning library*
-
-TODO
+*Tutorials*
 
 {include 0 Manual.Pages.DefiningAlgorithm}