Prove rdist_triangle

[Paul-Lez]

In this PR we prove the Ruzsa triangle inequality

[teorth]

I think you modified the hypotheses of rdist_triangle slightly and this has caused the usage of rdist_triangle at HundredPercent.lean to be slightly off, see https://github.com/teorth/pfr/actions/runs/6960892058/job/18942193897?pr=60 . Are you able to edit HundredPercent.lean to make it compile again? If not I can try to fix it on my end.

[Paul-Lez]

I should be able to edit it - I'm looking at it now. There seem to be other errors that are appearing (locally at least) in ruzsa_distance.lean - I'll try and fix these up and then push again!

[Paul-Lez]

Hopefully this should work now!

[teorth]

Still problematic unfortunately: https://github.com/teorth/pfr/actions/runs/6961920652/job/18944615099

[Paul-Lez]

That's weird - it worked locally. I'll have a look to see what's wrong with it

[Paul-Lez]

That's weird - it worked locally. I'll have a look to see what's wrong with it

I just realized I made some arguments implicit and forgot to make the corresponding modifications to HundredPercent.lean.
This should now work (the project builds locally anyway)

[teorth]

So sorry, it's still reporting an issue: https://github.com/teorth/pfr/actions/runs/6962400483/job/18946551993?pr=60

[collares]

GitHub CI for PR runs on a synthetic merge between the branch and master (in this particular case, the "Checkout project" build step for the latest CI run reports HEAD is now at 840c543 Merge 06a3d55ca4af7f91af6ed49e3cdfb7c825152716 into 626191a292bdb036af8031b655cb2be3b5f57515). This is very confusing if you're not aware of it.

@Paul-Lez If you merge master, you will see the errors locally too. In fact, you'll see more errors than in this PR's last CI run, because of newer commits on master.

[Paul-Lez]

I still need to make sure everything is fixed locally so it might be worth waiting a bit before running the CI

[Paul-Lez]

Seems like the build failed again - I'll try and see what caused this

[teorth]

Seems like the build failed again - I'll try and see what caused this

Oof, that's frustrating but it does seem like the error messages are different at least so there is progress...

[Paul-Lez]

Ah I think I found what happened! The hypotheses for independent_copies3_nondep changed, but I didn't get an error on my side (I've been having issues with cache files not updating correctly so I think this might be the root cause!)

[Paul-Lez]

Okay so what was causing an issue is that independent_copies3_nondep requires the measures to be probability measures. I've propagated the changes to the results that use Ruzsa triangle inequality, although I had to use sorry to get one of the instances in entropic_PFR_conjecture' (I'm guessing that entropic_PFR_conjecture should maybe give that too?).

The other sorry I added to entropic_PFR_conjecture' is that the uniform variable U should be measurable. I didn't find that fact in the API for uniform variables, but I'm happy to add it in a separate PR!

[Paul-Lez]

Looks like the build finished with no errors this time!

[teorth]

Yay! It worked. You should comment on the Zulip on the changes so that other people can fix the relevant sorries.