OAI/Probability/GammaPassage/RationalMeanAlgebra.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.rationalLatticePoint_scale line 10
2. lemma OAI.GammaFPP.rationalLatticePoint_add line 15
3. lemma OAI.GammaFPP.rationalLatticePoint_neg line 19
4. lemma OAI.GammaFPP.rationalPair_common_denominator line 25

   Source documentation

   Simultaneous positive common denominator, without canonical-denominator identities for addition or subtraction.

   lemma rationalPair_common_denominator (q r : ℚ × ℚ) :
       ∃ n : ℕ, 0 < n ∧ ∃ x y : Vertex,
         q = rationalLatticePoint x n ∧ r = rationalLatticePoint y n := by
   …

   Mentions: OAI.GammaFPP.rationalLatticePoint

5. lemma OAI.GammaFPP.rationalMean_zero line 38
6. lemma OAI.GammaFPP.rationalMean_add_le line 44
7. lemma OAI.GammaFPP.rationalMean_neg line 54
8. lemma OAI.GammaFPP.rationalLatticePoint_rat_smul line 63
9. lemma OAI.GammaFPP.rationalMean_smul line 81

   Source documentation

   Signed rational scalars include zero; positivity is needed only for the canonical denominator, never for the numerator.

   lemma rationalMean_smul (m : Vertex → ℝ)
       (hn : ∀ (k : ℕ) (x : Vertex), m (k • x) = (k : ℝ)*m x)
       (hz : ∀ (k : ℤ) (x : Vertex), m (k • x) = (k.natAbs : ℝ)*m x)
       (a : ℚ) (q : ℚ × ℚ) :
       rationalMean m (a • q) = |(a : ℝ)| * rationalMean m q := by
   …

   Mentions: OAI.GammaFPP.rationalMean

10. lemma OAI.GammaFPP.rationalLatticePoint_real_l1 line 99

    Source documentation

    Exact L1 distance for a positive common denominator.

    lemma rationalLatticePoint_real_l1 (x y : Vertex) (n : ℕ) (hn : 0 < n) :
        |((rationalLatticePoint x n).1 : ℝ)-((rationalLatticePoint y n).1 : ℝ)| +
          |((rationalLatticePoint x n).2 : ℝ)-((rationalLatticePoint y n).2 : ℝ)| =
          (((x.1-y.1).natAbs+(x.2-y.2).natAbs : ℕ) : ℝ)/(n : ℝ) := by
    …

    Mentions: OAI.GammaFPP.rationalLatticePoint

11. lemma OAI.GammaFPP.rationalMean_l1 line 107