Skip to content

Commit 3928f2b

Browse files
YaelDilliesYaelDillies
committed
Adopt the module system
1 parent d91e467 commit 3928f2b

69 files changed

Lines changed: 445 additions & 174 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎PFR/ApproxHomPFR.lean‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,11 @@
1-
import Mathlib.Data.FunLike.Fintype
2-
import Mathlib.Data.Int.Lemmas
1+
module
32

4-
import APAP.Extras.BSG
3+
public import Mathlib.Data.FunLike.Fintype
4+
public import Mathlib.Data.Int.Lemmas
55

6-
import PFR.HomPFR
6+
public import APAP.Extras.BSG
7+
8+
public import PFR.HomPFR
79

810
/-!
911
# The approximate homomorphism form of PFR
@@ -19,6 +21,8 @@ is true for a positive proportion of x,y.
1921
and a constant $c$ such that $f(x)=\phi(x)+c$ for a substantial set of values.
2022
-/
2123

24+
public section
25+
2226
open Finset Module
2327
open scoped Pointwise Combinatorics.Additive
2428

@@ -305,7 +309,3 @@ theorem approx_hom_pfr' (f : G → G') (K : ℝ) (hK : K > 0)
305309
ZeroHom.coe_mk, and_imp, A, φ'c]
306310
intro h1 h2
307311
simp [h1, h2]
308-
309-
/-- info: 'approx_hom_pfr'' depends on axioms: [propext, Classical.choice, Quot.sound] -/
310-
#guard_msgs in
311-
#print axioms approx_hom_pfr'

‎PFR/BoundingMutual.lean‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
1-
import Mathlib.Algebra.BigOperators.Group.Multiset.Defs
2-
import PFR.Mathlib.Data.Fin.Basic
3-
import PFR.MultiTauFunctional
1+
module
2+
3+
public import Mathlib.Algebra.BigOperators.Group.Multiset.Defs
4+
public import PFR.Mathlib.Data.Fin.Basic
5+
public import PFR.MultiTauFunctional
46

57
/-!
68
# Bounding the mutual information
79
-/
810

11+
public section
12+
913
universe u
1014
open MeasureTheory ProbabilityTheory
1115

‎PFR/Endgame.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
1-
import PFR.FirstEstimate
2-
import PFR.SecondEstimate
1+
module
2+
3+
public import PFR.FirstEstimate
4+
public import PFR.SecondEstimate
35

46
/-!
57
# Endgame
@@ -28,6 +30,8 @@ Assumptions:
2830
given some random variables with control on total cost, as well as total mutual information.
2931
-/
3032

33+
public section
34+
3135
open MeasureTheory ProbabilityTheory
3236

3337
variable {G : Type*} [AddCommGroup G] [Finite G] [hG : MeasurableSpace G]

‎PFR/EntropyPFR.lean‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
1-
import Mathlib.Algebra.Module.ZMod
2-
import PFR.TauFunctional
3-
import PFR.HundredPercent
4-
import PFR.Endgame
1+
module
2+
3+
public import Mathlib.Algebra.Module.ZMod
4+
public import PFR.TauFunctional
5+
public import PFR.HundredPercent
6+
public import PFR.Endgame
57

68
/-!
79
# Entropic version of polynomial Freiman-Ruzsa conjecture
@@ -15,6 +17,8 @@ Here we prove the entropic version of the polynomial Freiman-Ruzsa conjecture.
1517
1618
-/
1719

20+
public section
21+
1822
open MeasureTheory ProbabilityTheory
1923
universe uG
2024

‎PFR/Examples.lean‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@ import PFR.ImprovedPFR
33
import PFR.WeakPFR
44
import PFR.RhoFunctional
55

6+
public section
7+
68
section PFR
79

810
open Pointwise
@@ -212,3 +214,7 @@ example {Ω Ω' : Type*} [MeasurableSpace Ω] (ν : Measure Ω) [IsFiniteMeasure
212214
(ν.prod ν') E < ∞ := by finiteness
213215

214216
end Finiteness
217+
218+
/-- info: 'approx_hom_pfr'' depends on axioms: [propext, Classical.choice, Quot.sound] -/
219+
#guard_msgs in
220+
#print axioms approx_hom_pfr'

‎PFR/Fibring.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
1-
import PFR.ForMathlib.Entropy.RuzsaDist
1+
module
2+
3+
public import PFR.ForMathlib.Entropy.RuzsaDist
24

35
/-!
46
# The fibring identity
@@ -13,6 +15,8 @@ The proof of the fibring identity, which is a key component of the proof of PFR.
1315
1416
-/
1517

18+
public section
19+
1620
open MeasureTheory ProbabilityTheory Function
1721

1822
section GeneralFibring

‎PFR/FirstEstimate.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
1-
import PFR.Fibring
2-
import PFR.TauFunctional
1+
module
2+
3+
public import PFR.Fibring
4+
public import PFR.TauFunctional
35

46
/-!
57
# First estimate
@@ -21,6 +23,8 @@ Assumptions:
2123
(2 + \eta) k - I_1.$
2224
-/
2325

26+
public section
27+
2428
open MeasureTheory ProbabilityTheory
2529

2630
variable {G : Type*} [addgroup : AddCommGroup G] [Finite G] [hG : MeasurableSpace G]

‎PFR/ForMathlib/AffineSpaceDim.lean‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,11 @@
1-
import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
2-
import Mathlib.LinearAlgebra.Dimension.Constructions
3-
import Mathlib.LinearAlgebra.Dimension.Finite
4-
import PFR.Mathlib.LinearAlgebra.Dimension.Finrank
1+
module
2+
3+
public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
4+
public import Mathlib.LinearAlgebra.Dimension.Constructions
5+
public import Mathlib.LinearAlgebra.Dimension.Finite
6+
public import PFR.Mathlib.LinearAlgebra.Dimension.Finrank
7+
8+
@[expose] public section
59

610
open scoped Pointwise
711

‎PFR/ForMathlib/ConditionalIndependence.lean‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,11 @@
1-
import Mathlib.Tactic.Finiteness
2-
import PFR.Mathlib.Probability.IdentDistrib
3-
import PFR.ForMathlib.FiniteRange.ConditionalProbability
4-
import PFR.ForMathlib.Pair
1+
module
2+
3+
public import Mathlib.Tactic.Finiteness
4+
public import PFR.Mathlib.Probability.IdentDistrib
5+
public import PFR.ForMathlib.FiniteRange.ConditionalProbability
6+
public import PFR.ForMathlib.Pair
7+
8+
@[expose] public section
59

610
open MeasureTheory Measure Set
711
open scoped ENNReal

‎PFR/ForMathlib/Entropy/Basic.lean‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
1-
import PFR.ForMathlib.ConditionalIndependence
2-
import PFR.ForMathlib.Entropy.Kernel.MutualInfo
3-
import PFR.ForMathlib.Uniform
4-
import PFR.Mathlib.Probability.ConditionalProbability
1+
module
2+
3+
public import PFR.ForMathlib.ConditionalIndependence
4+
public import PFR.ForMathlib.Entropy.Kernel.MutualInfo
5+
public import PFR.ForMathlib.Uniform
6+
public import PFR.Mathlib.Probability.ConditionalProbability
57

68
/-!
79
# Entropy and conditional entropy
@@ -32,6 +34,8 @@ supposed to be `volume`). For example `H[X ; μ]` and `I[X : Y ; μ]` instead of
3234
3335
-/
3436

37+
@[expose] public section
38+
3539
open Function MeasureTheory Measure Real
3640
open scoped ENNReal NNReal Topology ProbabilityTheory
3741

0 commit comments

Comments
 (0)