RationalMean.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.rationalLatticePoint line 13
Source documentation
A rational pair represented by one positive natural denominator.
```
def rationalLatticePoint (x : Vertex) (n : ℕ) : ℚ × ℚ :=
…
```
def OAI.GammaFPP.rationalDenominator line 16
def OAI.GammaFPP.rationalNumerator line 18
theorem OAI.GammaFPP.rationalDenominator_pos line 21
theorem OAI.GammaFPP.rationalLatticePoint_numerator_denominator line 25
Source documentation
Explicit common-denominator representation, including zero coordinates.
```
theorem rationalLatticePoint_numerator_denominator (q : ℚ × ℚ) :
    rationalLatticePoint (rationalNumerator q) (rationalDenominator q) = q := by
…
```
Mentions: OAI.GammaFPP.rationalLatticePoint, OAI.GammaFPP.rationalNumerator, OAI.GammaFPP.rationalDenominator
theorem OAI.GammaFPP.rationalLatticePoint_cross line 44
Source documentation
Equality of rational points yields equality after integer cross multiplication.
```
theorem rationalLatticePoint_cross {x y : Vertex} {n k : ℕ}
    (hn : 0 < n) (hk : 0 < k)
    (he : rationalLatticePoint x n = rationalLatticePoint y k) :
    k • x = n • y := by
…
```
Mentions: OAI.GammaFPP.rationalLatticePoint

theorem OAI.GammaFPP.latticeMean_div_eq_of_cross line 61

Source documentation

Denominator compatibility derived from homogeneity, not assumed as a premise.

theorem latticeMean_div_eq_of_cross (m : Vertex → ℝ)
    (hm : ∀ (k : ℕ) (x : Vertex), m (k • x) = (k : ℝ) * m x)
    {x y : Vertex} {n k : ℕ} (hn : 0 < n) (hk : 0 < k)
    (he : k • x = n • y) : m x / (n : ℝ) = m y / (k : ℝ) := by
…

def OAI.GammaFPP.rationalMean line 72
Source documentation
A concrete rational mean; no representative is chosen nonconstructively.
```
noncomputable def rationalMean (m : Vertex → ℝ) (q : ℚ × ℚ) : ℝ :=
…
```

theorem OAI.GammaFPP.rationalMean_rationalLatticePoint line 76

Source documentation

Evaluation at every integer pair over every positive natural denominator.

theorem rationalMean_rationalLatticePoint (m : Vertex → ℝ)
    (hm : ∀ (k : ℕ) (x : Vertex), m (k • x) = (k : ℝ) * m x)
    (x : Vertex) (n : ℕ) (hn : 0 < n) :
    rationalMean m (rationalLatticePoint x n) = m x / (n : ℝ) := by
…

Mentions: OAI.GammaFPP.rationalMean, OAI.GammaFPP.rationalLatticePoint

theorem OAI.GammaFPP.rationalMean_integerPair line 87

Source documentation

Literal agreement with the integer lattice (denominator one).

theorem rationalMean_integerPair (m : Vertex → ℝ)
    (hm : ∀ (k : ℕ) (x : Vertex), m (k • x) = (k : ℝ) * m x)
    (x : Vertex) : rationalMean m ((x.1 : ℚ), (x.2 : ℚ)) = m x := by
…

Mentions: OAI.GammaFPP.rationalMean