OAI/NumberTheory/TotientAsymptotic/PrefixGeometry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.g_convolution line 16
2. def OAI.TotientAsymptotic.prefixSlack line 37
3. lemma OAI.TotientAsymptotic.weighted_slack_identity line 40
4. def OAI.TotientAsymptotic.prefixMatrix line 77
5. lemma OAI.TotientAsymptotic.prefixMatrix_upper line 80
6. lemma OAI.TotientAsymptotic.prefixMatrix_det line 85
7. def OAI.TotientAsymptotic.prefixLinear line 89
8. lemma OAI.TotientAsymptotic.prefixLinear_det line 92
9. lemma OAI.TotientAsymptotic.prefixLinear_preserves_volume line 96
10. def OAI.TotientAsymptotic.prefixVector line 102
11. lemma OAI.TotientAsymptotic.prefixLinear_apply line 104
12. lemma OAI.TotientAsymptotic.prefixLinear_vector line 119
13. lemma OAI.TotientAsymptotic.prefixSlack_zero line 131
14. lemma OAI.TotientAsymptotic.weighted_prefix_vector line 138
15. def OAI.TotientAsymptotic.extendPrefix line 150

    Source documentation

    Coordinates indexed from one, extended by zero outside the prefix.

    def extendPrefix (N : ℕ) (u : Fin N → ℝ) (i : ℕ) : ℝ :=
    …

    Mentions: OAI.TotientAsymptotic.N

16. lemma OAI.TotientAsymptotic.prefixVector_extend line 153
17. lemma OAI.TotientAsymptotic.weighted_prefixLinear line 158
18. def OAI.TotientAsymptotic.prefixRegion line 165

    Source documentation

    The prefix inequalities for a fixed tail threshold, including index zero.

    def prefixRegion (N : ℕ) (B C₀ : ℝ) (C : Fin N → ℝ) : Set (Fin N → ℝ) :=
    …

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

19. def OAI.TotientAsymptotic.weightedSimplex line 169
20. lemma OAI.TotientAsymptotic.prefixRegion_eq_simplex_preimage line 173

    Source documentation

    The available slack is the top budget minus all weighted tail thresholds.

    lemma prefixRegion_eq_simplex_preimage (N : ℕ) (B C₀ : ℝ) (C : Fin N → ℝ) :
        prefixRegion N B C₀ C =
          (fun u => prefixLinear N u - C) ⁻¹'
            weightedSimplex N (B-C₀-∑ i : Fin N, g (i.val+1)*C i) := by
    …

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

21. lemma OAI.TotientAsymptotic.prefixAffine_preserves_volume line 186
22. lemma OAI.TotientAsymptotic.measurableSet_weightedSimplex line 196
23. theorem OAI.TotientAsymptotic.volume_prefixRegion line 206

    Source documentation

    Exact reduction of the prefix volume, valid for every fixed tail threshold.

    theorem volume_prefixRegion (N : ℕ) (B C₀ : ℝ) (C : Fin N → ℝ) :
        MeasureTheory.volume (prefixRegion N B C₀ C) =
          MeasureTheory.volume
            (weightedSimplex N (B-C₀-∑ i : Fin N, g (i.val+1)*C i)) := by
    …

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

24. lemma OAI.TotientAsymptotic.prefixRegion_intersection line 215

    Source documentation

    Simultaneous witnesses impose coordinatewise maximum tail thresholds.

    lemma prefixRegion_intersection {ι : Type*} (N : ℕ) (B : ℝ)
        (T : Finset ι) (hT : T.Nonempty) (C₀ : ι → ℝ) (C : ι → Fin N → ℝ) :
        {u | ∀ η ∈ T, u ∈ prefixRegion N B (C₀ η) (C η)} =
          prefixRegion N B (T.sup' hT C₀) (fun i => T.sup' hT (fun η => C η i)) := by
    …

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