Notation and updates

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

Update: I've managed to complete a first draft of the blueprint, in the sense that it now contains all the mathematical steps. Only a fraction of the lemmas are formally stated in Lean at present, but I can work on doing that soon.

Separately, I have been trying to implement some notation for pairs and for conditional Ruzsa distance to stop the notation from becoming extremely cluttered. For pairs I am currently using

def prod {Ω S T : Type*} ( X : Ω → S ) ( Y : Ω → T ) (ω : Ω) : S × T := (X ω, Y ω)

notation3:100 "⟨ " X " , " Y " ⟩" => prod X Y

though it has the downside that the angled brackets are occasionally interpreted as a constructor (in which case an extra pair of parentheses are needed). Another minor issue is that the docs#Measurable.prod_mk method does not directly establish measurability of ⟨ X, Y ⟩ without first applying unfold prod, so I had to add a wrapper mes_prod_mk to fix this.

For the Ruzsa distance between two random variables X, Y associated with probability measures μ, μ' I am trialing

notation3:max "d[" X " ; " μ " # " Y " ; " μ' "]" => rdist X Y μ μ'

and for conditional Ruzsa distance I am trialing

notation3:max "d[" X " | " Z " ; " μ " # " Y " | " W " ; " μ' "]" => cond_rdist X Z Y W μ μ'

so that a typical result about Ruzsa distance (https://teorth.github.io/pfr/blueprint/sect0003.html#cond-dist-alt) now looks like this:

lemma cond_rdist_of_indep [MeasurableSpace S] [MeasurableSpace T] {X : Ω → G} {Z : Ω → S} {Y : Ω → G} {W : Ω → T} (h : IndepFun (⟨X, Z⟩) (⟨ Y, W ⟩) μ) : d[ X | Z ; μ # Y | W ; μ] = H[X-Y | ⟨ Z, W ⟩; μ ] - H[X | Z; μ ]/2 - H[Y | W; μ ]/2 := by sorry

This is something of a mess, but it was even worse without the above notational abbreviations.
I'm not completely sold on using # as a delimiter, but I couldn't think of a better choice right now (in the paper we use semicolons, but that delimiter has now been repurposed to specify the measure). Any suggestions are of course welcome.

[Kyle Miller]

I'm not sure if the spacing is intentional, but just to mention it, the spaces before and after quoted tokens in notation is a pretty printing hint for where to insert a space (and it's worth mentioning it has no impact on parsing). For example,

notation3:max "d[" X "; " μ " # " Y "; " μ' "]" => rdist X Y μ μ'

would print things like d[X; μ # Y; μ'] instead of d[X ; μ # Y ; μ'].

Since throwing out notation suggestions is fun, perhaps d[X; μ ;; Y; μ']?

[Mario Carneiro]

I see some issues with hyphens in lean definitions, for example rusza-triangle is listed as the lean name, which leads to a 404 because the real name is rusza_triangle

[Terence Tao]

Thanks for the pointers and heads up! I think I fixed all the hyphens in the Lean links, and reduced the whitespace in the notation.

[Kyle Miller]

For pairs, you could do something like

notation3:100 "p(" X ", " Y ")" => prod X Y

to avoid conflicts with angle bracket notation. Having no whitespace between an identifier and ( is reserved for notations and macros.

[Kyle Miller]

Re the minor issue about unfolding, you could make prod be an abbrev instead of a def. (abbrev is the same as def but it makes the definition become more transparent in many computations)