From 5d498663483e5f4af69a40f9e17b264fbe94ac33 Mon Sep 17 00:00:00 2001 From: teorth Date: Sun, 10 Dec 2023 08:35:00 -0800 Subject: [PATCH] add example --- examples.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/examples.lean b/examples.lean index eb3866fe..88720174 100644 --- a/examples.lean +++ b/examples.lean @@ -1,5 +1,6 @@ import Mathlib.Probability.Notation import PFR.Homomorphism +import PFR.ApproxHomomorphism import PFR.ImprovedPFR import PFR.ForMathlib.MeasureReal @@ -32,7 +33,13 @@ example (f : G → G') (S : Set G') (hS : ∀ x y : G, f (x + y) - f x - f y ∈ convert homomorphism_pfr f S hS norm_cast --- TODO: the approximate homomorphism version of PFR +-- Todo: replace the constants C₁, C₂, C₃, C₄ below with actual values + +/-- The approximate homomorphism version of PFR -/ +example (f : G → G') (K : ℝ) (hK: K > 0) (hf: Nat.card { x : G × G| f (x.1+x.2) = (f x.1) + (f x.2) } ≥ (Nat.card G)^2/ K) : ∃ (φ : G →+ G') (c : G'), Nat.card { x : G | f x = φ x + c } ≥ (Nat.card G) / (4 * C₁^25 * C₃^24 * K^(50 * C₄ + 48 * C₂)) := by + convert approx_hom_pfr f K hK hf + + end PFR