OAI/GroupTheory/PolycyclicRecognition/Analysis/IdealSectionBoxCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact linear coordinates for an ideal and its quotient

Pure quotient lifts have weight zero. In the adapted basis, projection retains exactly those coordinates, and inclusion of the ideal retains exactly the weighted ideal coordinates. This is the linear part of the section-coordinate box comparison.

  1. def OAI.PolycyclicRecognition.quotientLinearSection line 23
  2. theorem OAI.PolycyclicRecognition.quotientLinearSection_rightInverse line 26
  3. theorem OAI.PolycyclicRecognition.quotientLinearSection_repr_inl line 35
  4. theorem OAI.PolycyclicRecognition.quotientLinearSection_repr_inr line 51
  5. theorem OAI.PolycyclicRecognition.ideal_scaled_coordinates_le_iff line 59

    Source documentation

    Inclusion of the ideal is an isometry for the weighted coordinate norms.

    theorem ideal_scaled_coordinates_le_iff (s : I → ℝ) (r R : ℝ) (hR : 0 ≤ R) (u : U) :
    ‖(exponentialRescaleBasis
      (basisWithQuotientLifts U.toSubmodule bI bQ lift hlift)
      (Sum.elim s (fun _ => 0)) r).equivFun (u : V)‖ ≤ R ↔
    ‖(exponentialRescaleBasis bI s r).equivFun u‖ ≤ R := by
…

    Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.basisWithQuotientLifts

  6. theorem OAI.PolycyclicRecognition.quotient_scaled_coordinates_le line 86

    Source documentation

    Projection to the quotient never enlarges the adapted coordinate bound.

    theorem quotient_scaled_coordinates_le (s : I → ℝ) (r R : ℝ) (hR : 0 ≤ R)
    (v : V) (hv : ‖(exponentialRescaleBasis
      (basisWithQuotientLifts U.toSubmodule bI bQ lift hlift)
      (Sum.elim s (fun _ => 0)) r).equivFun v‖ ≤ R) :
    ‖bQ.equivFun (U.toSubmodule.mkQ v)‖ ≤ R := by
…

    Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.basisWithQuotientLifts

  7. theorem OAI.PolycyclicRecognition.section_scaled_coordinates_le line 99

    Source documentation

    A quotient log ball lifts into the zero-width part of every adapted box.

    theorem section_scaled_coordinates_le (s : I → ℝ) (r R : ℝ) (hR : 0 ≤ R)
    (q : V ⧸ U.toSubmodule) (hq : ‖bQ.equivFun q‖ ≤ R) :
    ‖(exponentialRescaleBasis
      (basisWithQuotientLifts U.toSubmodule bI bQ lift hlift)
      (Sum.elim s (fun _ => 0)) r).equivFun (quotientLinearSection U bQ lift q)‖ ≤ R := by
…

    Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.basisWithQuotientLifts, OAI.PolycyclicRecognition.quotientLinearSection