OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanOrdinaryBoxCover.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed larger boxes cover the differences of ordinary chart samples

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_ordinary_box_difference_cover line 29
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.groupBox_subset_positive_enlargement line 56

    Source documentation

    Nonnegative support widths imply inclusion in every positive homothetic enlargement without changing the coordinate radius.

    theorem groupBox_subset_positive_enlargement
    {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    (hweights : ∀ i, 0 < (M.supportIn T hunimod eW).weightSupport E i)
    (β : M.Bases) {r δ R : ℝ} (hr : 0 ≤ r) (hδ : 0 ≤ δ) :
    M.groupBox T hunimod eW (Exp ∘ eN) E β r R ⊆
      M.groupBox T hunimod eW (Exp ∘ eN) ((fun w => (1 + δ) • w) '' E) β r R := by
…