OAI/NumberTheory/TotientAsymptotic/SimplexVolume.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.standardSimplex line 13
2. lemma OAI.TotientAsymptotic.measurableSet_standardSimplex line 16
3. def OAI.TotientAsymptotic.simplexSection line 26
4. lemma OAI.TotientAsymptotic.measurableSet_simplexSection line 29
5. lemma OAI.TotientAsymptotic.standardSimplex_succ_preimage line 41
6. lemma OAI.TotientAsymptotic.volume_standardSimplex_succ line 57
7. lemma OAI.TotientAsymptotic.volume_standardSimplex_zero line 75
8. lemma OAI.TotientAsymptotic.integral_simplex_power line 84
9. theorem OAI.TotientAsymptotic.volume_standardSimplex line 96
10. def OAI.TotientAsymptotic.weightedScale line 114
11. lemma OAI.TotientAsymptotic.weightedScale_apply line 117
12. lemma OAI.TotientAsymptotic.weightedScale_det line 121
13. lemma OAI.TotientAsymptotic.weightedScale_det_pos line 125
14. lemma OAI.TotientAsymptotic.weightedSimplex_eq_preimage line 129
15. lemma OAI.TotientAsymptotic.volume_weightedSimplex_nonneg line 137
16. lemma OAI.TotientAsymptotic.volume_weightedSimplex line 151
17. theorem OAI.TotientAsymptotic.volume_prefixRegion_explicit line 168

    Source documentation

    The explicit determinant-one prefix volume formula from the manuscript.

    theorem volume_prefixRegion_explicit (N : ℕ) (hN : 0 < N)
        (B C₀ : ℝ) (C : Fin N → ℝ) :
        volume (prefixRegion N B C₀ C) =
          ENNReal.ofReal ((max (B-C₀-∑ i : Fin N, g (i.val+1)*C i) 0)^N /
            ((N.factorial : ℝ) * ∏ i : Fin N, g (i.val+1))) := by
    …

    Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.prefixRegion, OAI.TotientAsymptotic.g