OAI/GroupTheory/PolycyclicRecognition/Algebra/UnitNetPartition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.finite_subtype_unit_net_ball line 19
2. def OAI.PolycyclicRecognition.unitNetMass line 29
3. theorem OAI.PolycyclicRecognition.unitNetMass_apply line 39
4. theorem OAI.PolycyclicRecognition.mem_support_unitNetMass_iff line 42
5. def OAI.PolycyclicRecognition.unitNetTotal line 54
6. def OAI.PolycyclicRecognition.unitNetPartition line 56
7. theorem OAI.PolycyclicRecognition.unitNetMass_nonneg line 59
8. theorem OAI.PolycyclicRecognition.one_le_unitNetTotal line 62
9. theorem OAI.PolycyclicRecognition.unitNetPartition_nonneg line 72
10. theorem OAI.PolycyclicRecognition.unitNetPartition_total line 76
11. theorem OAI.PolycyclicRecognition.unitNetTotal_eq_sum line 85
12. theorem OAI.PolycyclicRecognition.cutoffPartition_eq_unitNetPartition line 92

    Source documentation

    On any finite set containing the support, the global partition agrees with the finite-dimensional cutoff partition.

    theorem cutoffPartition_eq_unitNetPartition (x : X) (s : Finset V)
        (hs : (unitNetMass hV x).support ⊆ s) (v : s) :
        cutoffPartition (fun u : s => (u.val : X)) x v = unitNetPartition hV x v.val := by
    …

    Mentions: OAI.PolycyclicRecognition.unitNetMass, OAI.PolycyclicRecognition.cutoffPartition, OAI.PolycyclicRecognition.unitNetPartition

13. theorem OAI.PolycyclicRecognition.unitNetPartition_variation_on_finset line 104
14. theorem OAI.PolycyclicRecognition.unitNetMass_support_card_le line 124
15. theorem OAI.PolycyclicRecognition.unitNetPartition_variation_le line 144

    Source documentation

    The infinite partition obeys the same sum-norm estimate as its finite restrictions. Only the two finite supports participate in the comparison.

    theorem unitNetPartition_variation_le
        (hcover : ∀ x : X, ∃ v ∈ V, dist x v ≤ 1) {M : ℕ}
        (hM : ∀ x : X, (V ∩ closedBall x 2).ncard ≤ M) (x y : X) :
        (unitNetPartition hV x - unitNetPartition hV y).sum (fun _ a => |a|) ≤
          4 * (M : ℝ) * dist x y := by
    …

    Mentions: OAI.PolycyclicRecognition.unitNetPartition