\n",
@@ -705,10 +725,10 @@
"id": "cell-08",
"metadata": {
"papermill": {
- "duration": 0.002245,
- "end_time": "2026-08-20T23:43:44.546427+00:00",
+ "duration": 0.002803,
+ "end_time": "2026-10-23T14:48:03.861958+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:44.544182+00:00",
+ "start_time": "2026-10-23T14:48:03.859155+00:00",
"status": "completed"
},
"tags": []
@@ -745,16 +765,16 @@
"id": "cell-09",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-08-20T23:43:44.551953Z",
- "iopub.status.busy": "2026-08-20T23:43:44.551778Z",
- "iopub.status.idle": "2026-08-20T23:43:44.739590Z",
- "shell.execute_reply": "2026-08-20T23:43:44.738762Z"
+ "iopub.execute_input": "2026-10-23T14:48:03.870568Z",
+ "iopub.status.busy": "2026-10-23T14:48:03.870291Z",
+ "iopub.status.idle": "2026-10-23T14:48:04.106664Z",
+ "shell.execute_reply": "2026-10-23T14:48:04.104950Z"
},
"papermill": {
- "duration": 0.191545,
- "end_time": "2026-08-20T23:43:44.740172+00:00",
+ "duration": 0.241848,
+ "end_time": "2026-10-23T14:48:04.107538+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:44.548627+00:00",
+ "start_time": "2026-10-23T14:48:03.865690+00:00",
"status": "completed"
},
"tags": []
@@ -775,46 +795,46 @@
" -- Code 4.1 - La distance de Ruzsa (PFR.ForMathlib.Entropy.RuzsaDist) -- -- rdist X Y mesure la ressemblance informationnelle de deux lois : -- d[X ; Y] = H[X] + H[Y] - H[X + Y] pour copies independantes. -- d[X ; Y] = H[X - Y] - H[X]/2 - H[Y]/2 (X, Y independantes). -- rdist_def en est la definition ; IdentDistrib.rdist_congr la compatibilite -- au changement d'espace probabilise ; IndepFun.rdist_eq l'identite cle -- au changement d'espace probabilise ; IndepFun.rdist_eq l'identite cle -- pour fonctions independantes. # check @ rdist @ rdist : {Ω : Type u_1} → \n",
- " {Ω' : Type u_2} → \n",
+ "#check @ rdist @ rdist : {Ω : Type u_1} → \n",
+ " {Ω' : Type u_2} → \n",
" {G : Type u_3} → \n",
" [mΩ : MeasurableSpace Ω] → \n",
- " [mΩ' : MeasurableSpace Ω'] → \n",
+ " [mΩ' : MeasurableSpace Ω'] → \n",
" [hG : MeasurableSpace G] → \n",
" [AddCommGroup G] → \n",
" (Ω → G) → \n",
- " (Ω' → G) → \n",
- " autoParam (MeasureTheory. Measure Ω) rdist._ auto_1 → \n",
- " autoParam (MeasureTheory. Measure Ω') rdist._ auto_3 → ℝ # check @ rdist_def @ rdist_def : ∀ {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_3} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω']\n",
- " [hG : MeasurableSpace G] [inst : AddCommGroup G] (X : Ω → G) (Y : Ω' → G) (μ : MeasureTheory. Measure Ω)\n",
- " (μ' : MeasureTheory. Measure Ω'),\n",
- " d[X; μ # Y; μ'] = \n",
- " H[fun x => x. 1 - x. 2 ; (MeasureTheory. Measure. map X μ). prod (MeasureTheory. Measure. map Y μ')] - H[X; μ] / 2 - \n",
- " H[Y; μ'] / 2 # check @ ProbabilityTheory. IdentDistrib. rdist_congr @ ProbabilityTheory. IdentDistrib. rdist_congr : ∀ {Ω : Type u_1} {Ω' : Type u_2} {Ω'' : Type u_3} {Ω''' : Type u_4}\n",
- " {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory. Measure Ω} [mΩ' : MeasurableSpace Ω']\n",
- " {μ' : MeasureTheory. Measure Ω'} [mΩ'' : MeasurableSpace Ω''] {μ'' : MeasureTheory. Measure Ω''}\n",
- " [mΩ''' : MeasurableSpace Ω'''] {μ''' : MeasureTheory. Measure Ω'''} [hG : MeasurableSpace G] [inst : AddCommGroup G]\n",
- " {X : Ω → G} {Y : Ω' → G} {X' : Ω'' → G} {Y' : Ω''' → G},\n",
- " ProbabilityTheory. IdentDistrib X X' μ μ'' → \n",
- " ProbabilityTheory. IdentDistrib Y Y' μ' μ''' → d[X; μ # Y; μ'] = d[X'; μ'' # Y'; μ'''] # check @ ProbabilityTheory. IndepFun. rdist_eq @ ProbabilityTheory. IndepFun. rdist_eq : ∀ {Ω : Type u_1} {G : Type u_2} [mΩ : MeasurableSpace Ω]\n",
- " {μ : MeasureTheory. Measure Ω} [hG : MeasurableSpace G] [inst : AddCommGroup G] {X : Ω → G} [Countable G]\n",
- " [MeasurableSingletonClass G] [MeasureTheory. IsFiniteMeasure μ] {Y : Ω → G},\n",
- " ProbabilityTheory. IndepFun X Y μ → \n",
+ " (Ω' → G) → \n",
+ " autoParam (MeasureTheory.Measure Ω) rdist._auto_1 → \n",
+ " autoParam (MeasureTheory.Measure Ω') rdist._auto_3 → ℝ #check @ rdist_def @ rdist_def : ∀ {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_3} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω']\n",
+ " [hG : MeasurableSpace G] [inst : AddCommGroup G] (X : Ω → G) (Y : Ω' → G) (μ : MeasureTheory.Measure Ω)\n",
+ " (μ' : MeasureTheory.Measure Ω'),\n",
+ " d[X; μ # Y; μ'] = \n",
+ " H[fun x => x. 1 - x. 2 ; (MeasureTheory.Measure.map X μ). prod (MeasureTheory.Measure.map Y μ')] - H[X; μ] / 2 - \n",
+ " H[Y; μ'] / 2 #check @ ProbabilityTheory.IdentDistrib.rdist_congr @ ProbabilityTheory.IdentDistrib.rdist_congr : ∀ {Ω : Type u_1} {Ω' : Type u_2} {Ω'' : Type u_3} {Ω''' : Type u_4}\n",
+ " {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω']\n",
+ " {μ' : MeasureTheory.Measure Ω'} [mΩ'' : MeasurableSpace Ω''] {μ'' : MeasureTheory.Measure Ω''}\n",
+ " [mΩ''' : MeasurableSpace Ω'''] {μ''' : MeasureTheory.Measure Ω'''} [hG : MeasurableSpace G] [inst : AddCommGroup G]\n",
+ " {X : Ω → G} {Y : Ω' → G} {X' : Ω'' → G} {Y' : Ω''' → G},\n",
+ " ProbabilityTheory.IdentDistrib X X' μ μ'' → \n",
+ " ProbabilityTheory.IdentDistrib Y Y' μ' μ''' → d[X; μ # Y; μ'] = d[X'; μ'' # Y'; μ'''] #check @ ProbabilityTheory.IndepFun.rdist_eq @ ProbabilityTheory.IndepFun.rdist_eq : ∀ {Ω : Type u_1} {G : Type u_2} [mΩ : MeasurableSpace Ω]\n",
+ " {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [inst : AddCommGroup G] {X : Ω → G} [Countable G]\n",
+ " [MeasurableSingletonClass G] [MeasureTheory.IsFiniteMeasure μ] {Y : Ω → G},\n",
+ " ProbabilityTheory.IndepFun X Y μ → \n",
" Measurable X → Measurable Y → d[X; μ # Y; μ] = H[X - Y; μ] - H[X; μ] / 2 - H[Y; μ] / 2 # print axioms rdist_def ' rdist_def' depends on axioms: [propext, Classical. choice, Quot. sound] #print axioms rdist_def ' rdist_def' depends on axioms : [propext, Classical.choice, Quot.sound] --% env 3 \n",
"
\n",
" Raw input \n",
- " {\"cmd\": \"-- Code 4.1 - La distance de Ruzsa (PFR.ForMathlib.Entropy.RuzsaDist)\\n--\\n-- rdist X Y mesure la ressemblance informationnelle de deux lois :\\n-- d[X ; Y] = H[X] + H[Y] - H[X + Y] pour copies independantes.\\n-- rdist_def en est la definition ; IdentDistrib.rdist_congr la compatibilite\\n-- au changement d'espace probabilise ; IndepFun.rdist_eq l'identite cle\\n-- pour fonctions independantes.\\n\\n#check @rdist\\n#check @rdist_def\\n#check @ProbabilityTheory.IdentDistrib.rdist_congr\\n#check @ProbabilityTheory.IndepFun.rdist_eq\\n#print axioms rdist_def\", \"env\": 2}\n",
+ " {\"cmd\": \"-- Code 4.1 - La distance de Ruzsa (PFR.ForMathlib.Entropy.RuzsaDist)\\n--\\n-- rdist X Y mesure la ressemblance informationnelle de deux lois :\\n-- d[X ; Y] = H[X - Y] - H[X]/2 - H[Y]/2 (X, Y independantes).\\n-- rdist_def en est la definition ; IdentDistrib.rdist_congr la compatibilite\\n-- au changement d'espace probabilise ; IndepFun.rdist_eq l'identite cle\\n-- pour fonctions independantes.\\n\\n#check @rdist\\n#check @rdist_def\\n#check @ProbabilityTheory.IdentDistrib.rdist_congr\\n#check @ProbabilityTheory.IndepFun.rdist_eq\\n#print axioms rdist_def\", \"env\": 2}\n",
" \n",
"
\n",
" Raw output \n",
@@ -852,7 +872,7 @@
"-- Code 4.1 - La distance de Ruzsa (PFR.ForMathlib.Entropy.RuzsaDist)\n",
"--\n",
"-- rdist X Y mesure la ressemblance informationnelle de deux lois :\n",
- "-- d[X ; Y] = H[X] + H[Y] - H[X + Y] pour copies independantes.\n",
+ "-- d[X ; Y] = H[X - Y] - H[X]/2 - H[Y]/2 (X, Y independantes).\n",
"-- rdist_def en est la definition ; IdentDistrib.rdist_congr la compatibilite\n",
"-- au changement d'espace probabilise ; IndepFun.rdist_eq l'identite cle\n",
"-- pour fonctions independantes.\n",
@@ -895,7 +915,7 @@
"--% env 3\n",
"\n",
"Raw input:\n",
- "{\"cmd\": \"-- Code 4.1 - La distance de Ruzsa (PFR.ForMathlib.Entropy.RuzsaDist)\\n--\\n-- rdist X Y mesure la ressemblance informationnelle de deux lois :\\n-- d[X ; Y] = H[X] + H[Y] - H[X + Y] pour copies independantes.\\n-- rdist_def en est la definition ; IdentDistrib.rdist_congr la compatibilite\\n-- au changement d'espace probabilise ; IndepFun.rdist_eq l'identite cle\\n-- pour fonctions independantes.\\n\\n#check @rdist\\n#check @rdist_def\\n#check @ProbabilityTheory.IdentDistrib.rdist_congr\\n#check @ProbabilityTheory.IndepFun.rdist_eq\\n#print axioms rdist_def\", \"env\": 2}\n",
+ "{\"cmd\": \"-- Code 4.1 - La distance de Ruzsa (PFR.ForMathlib.Entropy.RuzsaDist)\\n--\\n-- rdist X Y mesure la ressemblance informationnelle de deux lois :\\n-- d[X ; Y] = H[X - Y] - H[X]/2 - H[Y]/2 (X, Y independantes).\\n-- rdist_def en est la definition ; IdentDistrib.rdist_congr la compatibilite\\n-- au changement d'espace probabilise ; IndepFun.rdist_eq l'identite cle\\n-- pour fonctions independantes.\\n\\n#check @rdist\\n#check @rdist_def\\n#check @ProbabilityTheory.IdentDistrib.rdist_congr\\n#check @ProbabilityTheory.IndepFun.rdist_eq\\n#print axioms rdist_def\", \"env\": 2}\n",
"Raw output:\n",
"{\"messages\":\r\n",
" [{\"severity\": \"info\",\r\n",
@@ -934,7 +954,7 @@
"-- Code 4.1 - La distance de Ruzsa (PFR.ForMathlib.Entropy.RuzsaDist)\n",
"--\n",
"-- rdist X Y mesure la ressemblance informationnelle de deux lois :\n",
- "-- d[X ; Y] = H[X] + H[Y] - H[X + Y] pour copies independantes.\n",
+ "-- d[X ; Y] = H[X - Y] - H[X]/2 - H[Y]/2 (X, Y independantes).\n",
"-- rdist_def en est la definition ; IdentDistrib.rdist_congr la compatibilite\n",
"-- au changement d'espace probabilise ; IndepFun.rdist_eq l'identite cle\n",
"-- pour fonctions independantes.\n",
@@ -951,10 +971,10 @@
"id": "cell-10",
"metadata": {
"papermill": {
- "duration": 0.002765,
- "end_time": "2026-08-20T23:43:44.745942+00:00",
+ "duration": 0.003299,
+ "end_time": "2026-10-23T14:48:04.114754+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:44.743177+00:00",
+ "start_time": "2026-10-23T14:48:04.111455+00:00",
"status": "completed"
},
"tags": []
@@ -990,16 +1010,16 @@
"id": "cell-11",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-08-20T23:43:44.752433Z",
- "iopub.status.busy": "2026-08-20T23:43:44.752255Z",
- "iopub.status.idle": "2026-08-20T23:43:44.931238Z",
- "shell.execute_reply": "2026-08-20T23:43:44.930524Z"
+ "iopub.execute_input": "2026-10-23T14:48:04.123413Z",
+ "iopub.status.busy": "2026-10-23T14:48:04.123138Z",
+ "iopub.status.idle": "2026-10-23T14:48:04.352461Z",
+ "shell.execute_reply": "2026-10-23T14:48:04.350329Z"
},
"papermill": {
- "duration": 0.183244,
- "end_time": "2026-08-20T23:43:44.931837+00:00",
+ "duration": 0.235497,
+ "end_time": "2026-10-23T14:48:04.353912+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:44.748593+00:00",
+ "start_time": "2026-10-23T14:48:04.118415+00:00",
"status": "completed"
},
"tags": []
@@ -1017,19 +1037,19 @@
" \n",
" \n",
" \n",
- "
-- Code 5.1 - L'entropie binaire de Mathlib (Real.binEntropy) \n",
+ "
-- Code 5.1 - L'entropie binaire de Mathlib (Real.binEntropy) \n",
"
-- \n",
"
-- La famille BinaryEntropy : definition, forme canonique, symetrie, \n",
"
-- cas degenerez, encadrement du maximum, stricte monotonie de part \n",
- "
-- et d'autre de 1/2. \n",
+ "
-- et d'autre de 1/2. \n",
"
\n",
- "
# check @ Real. binEntropy\n",
- "
# check @ Real. binEntropy_eq_negMulLog_add_negMulLog_one_sub Real. binEntropy_eq_negMulLog_add_negMulLog_one_sub : ∀ (p : ℝ), Real. binEntropy p = p. negMulLog + (1 - p). negMulLog \n",
- "
# check @ Real. binEntropy_two_inv_add Real. binEntropy_two_inv_add : ∀ (p : ℝ), Real. binEntropy (2 ⁻¹ + p) = Real. binEntropy (2 ⁻¹ - p) \n",
- "
# check @ Real. binEntropy_eq_zero @ Real. binEntropy_eq_zero : ∀ {p : ℝ}, Real. binEntropy p = 0 ↔ p = 0 ∨ p = 1 \n",
- "
# check @ Real. binEntropy_le_log_two @ Real. binEntropy_le_log_two : ∀ {p : ℝ}, Real. binEntropy p ≤ Real. log 2 \n",
- "
# check @ Real. binEntropy_eq_log_two @ Real. binEntropy_eq_log_two : ∀ {p : ℝ}, Real. binEntropy p = Real. log 2 ↔ p = 2 ⁻¹ \n",
- "
# print axioms Real. binEntropy_le_log_two ' Real. binEntropy_le_log_two' depends on axioms: [propext, Classical. choice, Quot. sound] \n",
+ "
#check @ Real.binEntropy\n",
+ "
#check @ Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub : ∀ (p : ℝ), Real.binEntropy p = p.negMulLog + (1 - p). negMulLog \n",
+ "
#check @ Real.binEntropy_two_inv_add Real.binEntropy_two_inv_add : ∀ (p : ℝ), Real.binEntropy (2 ⁻¹ + p) = Real.binEntropy (2 ⁻¹ - p) \n",
+ "
#check @ Real.binEntropy_eq_zero @ Real.binEntropy_eq_zero : ∀ {p : ℝ}, Real.binEntropy p = 0 ↔ p = 0 ∨ p = 1 \n",
+ "
#check @ Real.binEntropy_le_log_two @ Real.binEntropy_le_log_two : ∀ {p : ℝ}, Real.binEntropy p ≤ Real.log 2 \n",
+ "
#check @ Real.binEntropy_eq_log_two @ Real.binEntropy_eq_log_two : ∀ {p : ℝ}, Real.binEntropy p = Real.log 2 ↔ p = 2 ⁻¹ \n",
+ "
#print axioms Real.binEntropy_le_log_two ' Real.binEntropy_le_log_two' depends on axioms : [propext, Classical.choice, Quot.sound] \n",
"
--% env 4 \n",
"
\n",
@@ -1166,10 +1186,10 @@
"id": "cell-12",
"metadata": {
"papermill": {
- "duration": 0.002975,
- "end_time": "2026-08-20T23:43:44.937934+00:00",
+ "duration": 0.003424,
+ "end_time": "2026-10-23T14:48:04.361838+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:44.934959+00:00",
+ "start_time": "2026-10-23T14:48:04.358414+00:00",
"status": "completed"
},
"tags": []
@@ -1220,16 +1240,16 @@
"id": "cell-13",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-08-20T23:43:44.944981Z",
- "iopub.status.busy": "2026-08-20T23:43:44.944790Z",
- "iopub.status.idle": "2026-08-20T23:43:45.119141Z",
- "shell.execute_reply": "2026-08-20T23:43:45.118358Z"
+ "iopub.execute_input": "2026-10-23T14:48:04.376999Z",
+ "iopub.status.busy": "2026-10-23T14:48:04.376423Z",
+ "iopub.status.idle": "2026-10-23T14:48:04.610649Z",
+ "shell.execute_reply": "2026-10-23T14:48:04.609295Z"
},
"papermill": {
- "duration": 0.178827,
- "end_time": "2026-08-20T23:43:45.119664+00:00",
+ "duration": 0.245394,
+ "end_time": "2026-10-23T14:48:04.611821+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:44.940837+00:00",
+ "start_time": "2026-10-23T14:48:04.366427+00:00",
"status": "completed"
},
"tags": []
@@ -1250,27 +1270,29 @@
" -- Code 6.1 - Le moteur de descente et la conjecture entropique (PFR.EntropyPFR) -- -- tau_strictly_decreases : la fonctionnelle tau decroit strictement a chaque -- iteration -- c'est le moteur de la preuve. entropic_PFR_conjecture : la -- iteration -- c'est le moteur de la preuve. entropic_PFR_conjecture : la -- conjecture entropique (p.eta = 1/9 fixe le regime de presque-uniformite), -- dont PFR_conjecture (section 1) se deduit. # check @ tau_strictly_decreases @ tau_strictly_decreases : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory. MeasureSpace Ω₀₁]\n",
- " [inst_1 : MeasureTheory. MeasureSpace Ω₀₂] {Ω : Type u_4} [mΩ : MeasureTheory. MeasureSpace Ω]\n",
- " [MeasureTheory. IsProbabilityMeasure MeasureTheory. volume] [MeasureTheory. IsProbabilityMeasure MeasureTheory. volume]\n",
- " [MeasureTheory. IsProbabilityMeasure MeasureTheory. volume] {G : Type u_1} [inst_5 : AddCommGroup G] [Module (ZMod 2 ) G]\n",
+ "#check @ tau_strictly_decreases @ tau_strictly_decreases : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\n",
+ " [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω]\n",
+ " [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\n",
+ " [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_5 : AddCommGroup G] [Module (ZMod 2 ) G]\n",
" [Finite G] [inst_8 : MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) {X₁ X₂ : Ω → G},\n",
- " Measurable X₁ → Measurable X₂ → tau_minimizes p X₁ X₂ → p. η = 1 / 9 → d[X₁ # X₂] = 0 # check @ entropic_PFR_conjecture @ entropic_PFR_conjecture : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory. MeasureSpace Ω₀₁]\n",
- " [inst_1 : MeasureTheory. MeasureSpace Ω₀₂] [MeasureTheory. IsProbabilityMeasure MeasureTheory. volume]\n",
- " [MeasureTheory. IsProbabilityMeasure MeasureTheory. volume] {G : Type u_1} [inst_4 : AddCommGroup G]\n",
+ " Measurable X₁ → Measurable X₂ → TauMinimizes p X₁ X₂ → p.η = 1 / 9 → d[X₁ # X₂] = 0 #check @ entropic_PFR_conjecture @ entropic_PFR_conjecture : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\n",
+ " [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\n",
+ " [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_4 : AddCommGroup G]\n",
" [inst_5 : Module (ZMod 2 ) G] [Finite G] [inst_7 : MeasurableSpace G] [MeasurableSingletonClass G]\n",
" (p : refPackage Ω₀₁ Ω₀₂ G),\n",
- " p. η = 1 / 9 → \n",
+ " p.η = 1 / 9 → \n",
" ∃ H Ω mΩ U,\n",
- " MeasureTheory. IsProbabilityMeasure MeasureTheory. volume ∧ \n",
+ " MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ \n",
" Measurable U ∧ \n",
- " ProbabilityTheory. IsUniform (↑ H) U MeasureTheory. volume ∧ d[p. X₀₁ # U] + d[p. X₀₂ # U] ≤ 11 * d[p. X₀₁ # p. X₀₂] # print axioms entropic_PFR_conjecture ' entropic_PFR_conjecture' depends on axioms: [propext, Classical. choice, Quot. sound] ProbabilityTheory.IsUniform (↑ H) U MeasureTheory.volume ∧ \n",
+ " d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 11 * d[p.X₀₁ # p.X₀₂] ∧ \n",
+ " d[p.X₀₁ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] ∧ d[p.X₀₂ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] #print axioms entropic_PFR_conjecture ' entropic_PFR_conjecture' depends on axioms : [propext, Classical.choice, Quot.sound] --% env 5 \n",
@@ -1284,12 +1306,12 @@
" \"pos\": {\"line\": 8, \"column\": 0},\r\n",
" \"endPos\": {\"line\": 8, \"column\": 6},\r\n",
" \"data\":\r\n",
- " \"@tau_strictly_decreases : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\\n [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_5 : AddCommGroup G] [Module (ZMod 2) G]\\n [Finite G] [inst_8 : MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) {X₁ X₂ : Ω → G},\\n Measurable X₁ → Measurable X₂ → tau_minimizes p X₁ X₂ → p.η = 1 / 9 → d[X₁ # X₂] = 0\"},\r\n",
+ " \"@tau_strictly_decreases : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\\n [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_5 : AddCommGroup G] [Module (ZMod 2) G]\\n [Finite G] [inst_8 : MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) {X₁ X₂ : Ω → G},\\n Measurable X₁ → Measurable X₂ → TauMinimizes p X₁ X₂ → p.η = 1 / 9 → d[X₁ # X₂] = 0\"},\r\n",
" {\"severity\": \"info\",\r\n",
" \"pos\": {\"line\": 9, \"column\": 0},\r\n",
" \"endPos\": {\"line\": 9, \"column\": 6},\r\n",
" \"data\":\r\n",
- " \"@entropic_PFR_conjecture : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\\n [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_4 : AddCommGroup G]\\n [inst_5 : Module (ZMod 2) G] [Finite G] [inst_7 : MeasurableSpace G] [MeasurableSingletonClass G]\\n (p : refPackage Ω₀₁ Ω₀₂ G),\\n p.η = 1 / 9 →\\n ∃ H Ω mΩ U,\\n MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧\\n Measurable U ∧\\n ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 11 * d[p.X₀₁ # p.X₀₂]\"},\r\n",
+ " \"@entropic_PFR_conjecture : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\\n [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_4 : AddCommGroup G]\\n [inst_5 : Module (ZMod 2) G] [Finite G] [inst_7 : MeasurableSpace G] [MeasurableSingletonClass G]\\n (p : refPackage Ω₀₁ Ω₀₂ G),\\n p.η = 1 / 9 →\\n ∃ H Ω mΩ U,\\n MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧\\n Measurable U ∧\\n ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧\\n d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 11 * d[p.X₀₁ # p.X₀₂] ∧\\n d[p.X₀₁ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] ∧ d[p.X₀₂ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂]\"},\r\n",
" {\"severity\": \"info\",\r\n",
" \"pos\": {\"line\": 10, \"column\": 0},\r\n",
" \"endPos\": {\"line\": 10, \"column\": 6},\r\n",
@@ -1313,7 +1335,7 @@
" [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\n",
" [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_5 : AddCommGroup G] [Module (ZMod 2) G]\n",
" [Finite G] [inst_8 : MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) {X₁ X₂ : Ω → G},\n",
- " Measurable X₁ → Measurable X₂ → tau_minimizes p X₁ X₂ → p.η = 1 / 9 → d[X₁ # X₂] = 0\n",
+ " Measurable X₁ → Measurable X₂ → TauMinimizes p X₁ X₂ → p.η = 1 / 9 → d[X₁ # X₂] = 0\n",
"#check @entropic_PFR_conjecture\n",
"──────▶ @entropic_PFR_conjecture : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\n",
" [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\n",
@@ -1324,7 +1346,9 @@
" ∃ H Ω mΩ U,\n",
" MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧\n",
" Measurable U ∧\n",
- " ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 11 * d[p.X₀₁ # p.X₀₂]\n",
+ " ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧\n",
+ " d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 11 * d[p.X₀₁ # p.X₀₂] ∧\n",
+ " d[p.X₀₁ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] ∧ d[p.X₀₂ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂]\n",
"#print axioms entropic_PFR_conjecture\n",
"──────▶ 'entropic_PFR_conjecture' depends on axioms: [propext, Classical.choice, Quot.sound]\n",
"--% env 5\n",
@@ -1337,12 +1361,12 @@
" \"pos\": {\"line\": 8, \"column\": 0},\r\n",
" \"endPos\": {\"line\": 8, \"column\": 6},\r\n",
" \"data\":\r\n",
- " \"@tau_strictly_decreases : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\\n [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_5 : AddCommGroup G] [Module (ZMod 2) G]\\n [Finite G] [inst_8 : MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) {X₁ X₂ : Ω → G},\\n Measurable X₁ → Measurable X₂ → tau_minimizes p X₁ X₂ → p.η = 1 / 9 → d[X₁ # X₂] = 0\"},\r\n",
+ " \"@tau_strictly_decreases : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\\n [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_5 : AddCommGroup G] [Module (ZMod 2) G]\\n [Finite G] [inst_8 : MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) {X₁ X₂ : Ω → G},\\n Measurable X₁ → Measurable X₂ → TauMinimizes p X₁ X₂ → p.η = 1 / 9 → d[X₁ # X₂] = 0\"},\r\n",
" {\"severity\": \"info\",\r\n",
" \"pos\": {\"line\": 9, \"column\": 0},\r\n",
" \"endPos\": {\"line\": 9, \"column\": 6},\r\n",
" \"data\":\r\n",
- " \"@entropic_PFR_conjecture : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\\n [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_4 : AddCommGroup G]\\n [inst_5 : Module (ZMod 2) G] [Finite G] [inst_7 : MeasurableSpace G] [MeasurableSingletonClass G]\\n (p : refPackage Ω₀₁ Ω₀₂ G),\\n p.η = 1 / 9 →\\n ∃ H Ω mΩ U,\\n MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧\\n Measurable U ∧\\n ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 11 * d[p.X₀₁ # p.X₀₂]\"},\r\n",
+ " \"@entropic_PFR_conjecture : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\\n [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_4 : AddCommGroup G]\\n [inst_5 : Module (ZMod 2) G] [Finite G] [inst_7 : MeasurableSpace G] [MeasurableSingletonClass G]\\n (p : refPackage Ω₀₁ Ω₀₂ G),\\n p.η = 1 / 9 →\\n ∃ H Ω mΩ U,\\n MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧\\n Measurable U ∧\\n ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧\\n d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 11 * d[p.X₀₁ # p.X₀₂] ∧\\n d[p.X₀₁ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] ∧ d[p.X₀₂ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂]\"},\r\n",
" {\"severity\": \"info\",\r\n",
" \"pos\": {\"line\": 10, \"column\": 0},\r\n",
" \"endPos\": {\"line\": 10, \"column\": 6},\r\n",
@@ -1373,10 +1397,10 @@
"id": "cell-14",
"metadata": {
"papermill": {
- "duration": 0.002949,
- "end_time": "2026-08-20T23:43:45.125831+00:00",
+ "duration": 0.003583,
+ "end_time": "2026-10-23T14:48:04.620127+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:45.122882+00:00",
+ "start_time": "2026-10-23T14:48:04.616544+00:00",
"status": "completed"
},
"tags": []
@@ -1399,14 +1423,14 @@
"cell_type": "markdown",
"id": "cell-lean21-friction-8",
"metadata": {
- "tags": [],
"papermill": {
- "duration": 0.0,
- "end_time": "2026-09-12T21:30:00+00:00",
+ "duration": 0.003418,
+ "end_time": "2026-10-23T14:48:04.627017+00:00",
"exception": false,
- "start_time": "2026-09-12T21:30:00+00:00",
+ "start_time": "2026-10-23T14:48:04.623599+00:00",
"status": "completed"
- }
+ },
+ "tags": []
},
"source": [
"## 8. Friction et chemin de decouverte\n",
@@ -1422,14 +1446,14 @@
"cell_type": "markdown",
"id": "cell-lean21-friction-8-1",
"metadata": {
- "tags": [],
"papermill": {
- "duration": 0.0,
- "end_time": "2026-09-12T21:30:01+00:00",
+ "duration": 0.004281,
+ "end_time": "2026-10-23T14:48:04.635570+00:00",
"exception": false,
- "start_time": "2026-09-12T21:30:01+00:00",
+ "start_time": "2026-10-23T14:48:04.631289+00:00",
"status": "completed"
- }
+ },
+ "tags": []
},
"source": [
"### 8.1 Les obstacles connus - pourquoi la preuve a resiste\n",
@@ -1451,14 +1475,14 @@
"cell_type": "markdown",
"id": "cell-lean21-friction-8-2",
"metadata": {
- "tags": [],
"papermill": {
- "duration": 0.0,
- "end_time": "2026-09-12T21:30:02+00:00",
+ "duration": 0.004163,
+ "end_time": "2026-10-23T14:48:04.643288+00:00",
"exception": false,
- "start_time": "2026-09-12T21:30:02+00:00",
+ "start_time": "2026-10-23T14:48:04.639125+00:00",
"status": "completed"
- }
+ },
+ "tags": []
},
"source": [
"### 8.2 Le chemin de decouverte - ce qui marche vs ce qui bloque\n",
@@ -1486,7 +1510,17 @@
},
{
"cell_type": "markdown",
- "metadata": {},
+ "id": "1349d378",
+ "metadata": {
+ "papermill": {
+ "duration": 0.003426,
+ "end_time": "2026-10-23T14:48:04.655379+00:00",
+ "exception": false,
+ "start_time": "2026-10-23T14:48:04.651953+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
"source": [
"### 8.3 Dette residuelle - ce qui reste ouvert apres la preuve KAW\n",
"\n",
@@ -1508,10 +1542,10 @@
"id": "cell-15",
"metadata": {
"papermill": {
- "duration": 0.003308,
- "end_time": "2026-08-20T23:43:45.132379+00:00",
+ "duration": 0.003845,
+ "end_time": "2026-10-23T14:48:04.662716+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:45.129071+00:00",
+ "start_time": "2026-10-23T14:48:04.658871+00:00",
"status": "completed"
},
"tags": []
@@ -1527,10 +1561,10 @@
"id": "cell-16",
"metadata": {
"papermill": {
- "duration": 0.003057,
- "end_time": "2026-08-20T23:43:45.138519+00:00",
+ "duration": 0.003726,
+ "end_time": "2026-10-23T14:48:04.670123+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:45.135462+00:00",
+ "start_time": "2026-10-23T14:48:04.666397+00:00",
"status": "completed"
},
"tags": []
@@ -1553,16 +1587,16 @@
"id": "cell-17",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-08-20T23:43:45.145909Z",
- "iopub.status.busy": "2026-08-20T23:43:45.145727Z",
- "iopub.status.idle": "2026-08-20T23:43:45.313822Z",
- "shell.execute_reply": "2026-08-20T23:43:45.312795Z"
+ "iopub.execute_input": "2026-10-23T14:48:04.678774Z",
+ "iopub.status.busy": "2026-10-23T14:48:04.678506Z",
+ "iopub.status.idle": "2026-10-23T14:48:04.884751Z",
+ "shell.execute_reply": "2026-10-23T14:48:04.880516Z"
},
"papermill": {
- "duration": 0.172879,
- "end_time": "2026-08-20T23:43:45.314471+00:00",
+ "duration": 0.212799,
+ "end_time": "2026-10-23T14:48:04.886544+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:45.141592+00:00",
+ "start_time": "2026-10-23T14:48:04.673745+00:00",
"status": "completed"
},
"tags": []
@@ -1580,14 +1614,14 @@
" \n",
" \n",
" \n",
- "
-- Exercice 1 - Entropie d'une loi uniforme \n",
+ "
-- Exercice 1 - Entropie d'une loi uniforme \n",
"
-- Étape 1 : instancier entropy_le_log_card pour X uniforme sur A. \n",
- "
-- Étape 2 : montrer l'egalite H[X] = log |A| (masses egales). \n",
+ "
-- Étape 2 : montrer l'egalite H[X] = log |A| (masses egales). \n",
"
-- TODO etudiant \n",
"
\n",
- "
# check @ ProbabilityTheory. entropy_le_log_card\n",
"
--% env 6 \n",
"
\n",
@@ -1648,10 +1682,10 @@
"id": "cell-18",
"metadata": {
"papermill": {
- "duration": 0.003188,
- "end_time": "2026-08-20T23:43:45.321268+00:00",
+ "duration": 0.004335,
+ "end_time": "2026-10-23T14:48:04.897001+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:45.318080+00:00",
+ "start_time": "2026-10-23T14:48:04.892666+00:00",
"status": "completed"
},
"tags": []
@@ -1675,16 +1709,16 @@
"id": "cell-19",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-08-20T23:43:45.328710Z",
- "iopub.status.busy": "2026-08-20T23:43:45.328530Z",
- "iopub.status.idle": "2026-08-20T23:43:45.499963Z",
- "shell.execute_reply": "2026-08-20T23:43:45.499070Z"
+ "iopub.execute_input": "2026-10-23T14:48:04.905854Z",
+ "iopub.status.busy": "2026-10-23T14:48:04.905536Z",
+ "iopub.status.idle": "2026-10-23T14:48:05.131042Z",
+ "shell.execute_reply": "2026-10-23T14:48:05.129292Z"
},
"papermill": {
- "duration": 0.176182,
- "end_time": "2026-08-20T23:43:45.500540+00:00",
+ "duration": 0.233091,
+ "end_time": "2026-10-23T14:48:05.133767+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:45.324358+00:00",
+ "start_time": "2026-10-23T14:48:04.900676+00:00",
"status": "completed"
},
"tags": []
@@ -1709,7 +1743,7 @@
"-- Étape 3 : expliquer pourquoi le A dissocié ci-dessous donne K > 2. -- TODO etudiant # eval (sumset [1 , 2 , 4 , 8 , 16 , 32 ]). length -- amorce : |A+A| pour les 6 bases #eval (sumset [1 , 2 , 4 , 8 , 16 , 32 ]). length -- amorce : |A+A| pour les 6 bases --% env 7 \n",
@@ -1770,10 +1804,10 @@
"id": "cell-20",
"metadata": {
"papermill": {
- "duration": 0.003572,
- "end_time": "2026-08-20T23:43:45.507930+00:00",
+ "duration": 0.00391,
+ "end_time": "2026-10-23T14:48:05.142264+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:45.504358+00:00",
+ "start_time": "2026-10-23T14:48:05.138354+00:00",
"status": "completed"
},
"tags": []
@@ -1797,16 +1831,16 @@
"id": "cell-21",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-08-20T23:43:45.516023Z",
- "iopub.status.busy": "2026-08-20T23:43:45.515840Z",
- "iopub.status.idle": "2026-08-20T23:43:45.689180Z",
- "shell.execute_reply": "2026-08-20T23:43:45.687947Z"
+ "iopub.execute_input": "2026-10-23T14:48:05.152279Z",
+ "iopub.status.busy": "2026-10-23T14:48:05.152003Z",
+ "iopub.status.idle": "2026-10-23T14:48:05.360699Z",
+ "shell.execute_reply": "2026-10-23T14:48:05.358285Z"
},
"papermill": {
- "duration": 0.178497,
- "end_time": "2026-08-20T23:43:45.689867+00:00",
+ "duration": 0.215879,
+ "end_time": "2026-10-23T14:48:05.362015+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:45.511370+00:00",
+ "start_time": "2026-10-23T14:48:05.146136+00:00",
"status": "completed"
},
"tags": []
@@ -1824,13 +1858,13 @@
" \n",
" \n",
" \n",
- "
-- Exercice 3 - Maximum de l'entropie binaire \n",
+ "
-- Exercice 3 - Maximum de l'entropie binaire \n",
"
-- Étape 1 : binEntropy_le_log_two donne le plafond. \n",
- "
-- Étape 2 : binEntropy_eq_log_two caracterise l'egalite (p = 1/2). \n",
+ "
-- Étape 2 : binEntropy_eq_log_two caracterise l'egalite (p = 1/2). \n",
"
-- Étape 3 : binEntropy_eq_zero decrit les cas degenerez. \n",
"
-- TODO etudiant \n",
"
\n",
- "
# check @ Real. binEntropy_eq_log_two @ Real. binEntropy_eq_log_two : ∀ {p : ℝ}, Real. binEntropy p = Real. log 2 ↔ p = 2 ⁻¹ \n",
+ "
#check @ Real.binEntropy_eq_log_two @ Real.binEntropy_eq_log_two : ∀ {p : ℝ}, Real.binEntropy p = Real.log 2 ↔ p = 2 ⁻¹ \n",
"
--% env 8 \n",
"
\n",
@@ -1891,10 +1925,10 @@
"id": "cell-22",
"metadata": {
"papermill": {
- "duration": 0.004148,
- "end_time": "2026-08-20T23:43:45.698005+00:00",
+ "duration": 0.004387,
+ "end_time": "2026-10-23T14:48:05.370594+00:00",
"exception": false,
- "start_time": "2026-08-20T23:43:45.693857+00:00",
+ "start_time": "2026-10-23T14:48:05.366207+00:00",
"status": "completed"
},
"tags": []
@@ -1930,6 +1964,18 @@
"mimetype": "text/x-lean4",
"name": "lean4"
},
+ "papermill": {
+ "default_parameters": {},
+ "duration": 9.32352,
+ "end_time": "2026-10-23T14:48:05.794634+00:00",
+ "environment_variables": {},
+ "exception": null,
+ "input_path": "ANALYSE-03-PFR-Lean.ipynb",
+ "output_path": "ANALYSE-03-PFR-Lean.ipynb",
+ "parameters": {},
+ "start_time": "2026-10-23T14:47:56.471114+00:00",
+ "version": "2.7.0"
+ },
"title": "Lean-20 : La conjecture PFR (Gowers-Green-Manners-Tao) et la méthode entropique"
},
"nbformat": 4,