OAI/Probability/GammaPassage/RealMeanExtension.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.rationalPairCast line 16

   Source documentation

   The rational embedding uses the standard product (maximum) metric.

   def rationalPairCast (q : ℚ × ℚ) : ℝ × ℝ := ((q.1 : ℝ), (q.2 : ℝ))

2. lemma OAI.GammaFPP.rationalPairCast_uniformEmbedding line 18
3. lemma OAI.GammaFPP.rationalPairCast_dense line 21
4. lemma OAI.GammaFPP.rationalPairCast_add line 24
5. lemma OAI.GammaFPP.rationalPairCast_neg line 28
6. lemma OAI.GammaFPP.rationalPairCast_smul line 32
7. lemma OAI.GammaFPP.rational_l1_lipschitz line 37

   Source documentation

   L1 is at most twice the standard product maximum metric.

   lemma rational_l1_lipschitz (f : ℚ × ℚ → ℝ) (C : ℝ≥0)
       (h : ∀ q r, |f q-f r| ≤ (C : ℝ) *
         (|(q.1 : ℝ)-(r.1 : ℝ)| + |(q.2 : ℝ)-(r.2 : ℝ)|)) :
       LipschitzWith (2*C) f := by
   …

8. def OAI.GammaFPP.realMeanExtension line 51
9. lemma OAI.GammaFPP.realMeanExtension_uniformContinuous line 55
10. lemma OAI.GammaFPP.realMeanExtension_on_rat line 60
11. lemma OAI.GammaFPP.realMeanExtension_add_le line 66
12. lemma OAI.GammaFPP.realMeanExtension_neg line 80
13. lemma OAI.GammaFPP.realMeanExtension_smul line 92

    Source documentation

    Density in the scalar AND vector proves full real homogeneity.

    lemma realMeanExtension_smul {f : ℚ × ℚ → ℝ} (hf : UniformContinuous f)
        (hsmul : ∀ (a : ℚ) q, f (a • q) = |(a : ℝ)| * f q)
        (a : ℝ) (x : ℝ × ℝ) :
        realMeanExtension f (a • x) = |a| * realMeanExtension f x := by
    …

    Mentions: OAI.GammaFPP.realMeanExtension

14. def OAI.GammaFPP.realMeanSeminorm line 110

    Source documentation

    Construct, rather than assume, a real seminorm from rational data.

    noncomputable def realMeanSeminorm (f : ℚ × ℚ → ℝ) (C : ℝ≥0)
        (hlip : ∀ q r, |f q-f r| ≤ (C : ℝ) *
          (|(q.1 : ℝ)-(r.1 : ℝ)| + |(q.2 : ℝ)-(r.2 : ℝ)|))
        (hzero : f 0 = 0) (hadd : ∀ q r, f (q+r) ≤ f q + f r)
        (hneg : ∀ q, f (-q) = f q)
        (hsmul : ∀ (a : ℚ) q, f (a • q) = |(a : ℝ)| * f q) :
        Seminorm ℝ (ℝ × ℝ) where
    …

15. theorem OAI.GammaFPP.realMeanExtension_integerPair line 131

    Source documentation

    Agreement with the original lattice mean once its rational L1 bound is supplied. No seminorm or continuity premise on that lattice function is needed.

    theorem realMeanExtension_integerPair (m : PlanarFPP.Vertex → ℝ)
        (hm : ∀ (k : ℕ) (x : PlanarFPP.Vertex), m (k • x) = (k : ℝ) * m x)
        (C : ℝ≥0)
        (hlip : ∀ q r, |rationalMean m q-rationalMean m r| ≤ (C : ℝ) *
          (|(q.1 : ℝ)-(r.1 : ℝ)| + |(q.2 : ℝ)-(r.2 : ℝ)|))
        (x : PlanarFPP.Vertex) :
        realMeanExtension (rationalMean m) ((x.1 : ℝ), (x.2 : ℝ)) = m x := by
    …

    Mentions: OAI.PlanarFPP.Vertex, OAI.GammaFPP.rationalMean, OAI.GammaFPP.realMeanExtension