OAI/GroupTheory/PolycyclicRecognition/Geometry/CanonicalHeightMetricModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The published Lie-model reduction with its actual canonical height

  1. theorem OAI.PolycyclicRecognition.exists_canonical_height_metric_model line 19

    Source documentation

    The model reduction, faithful matrix differential, scalar integration and exponential chart supply a Euclidean canonical height. Metric compatibility is proved from the selected metric's chain property. No affine-height estimate is part of these published inputs.

    theorem exists_canonical_height_metric_model
    (ct : CornulierTesseraModelInput) (metric : GeodesicMetricExistenceInput)
    (differential : MatrixLieDifferentialInput)
    (dixmier : ∀ (R : SimplyConnectedSolvableLieModel) (d : ProperChainMetric R.carrier),
      letI := d.compatibleMetric
…

    Mentions: OAI.PolycyclicRecognition.CornulierTesseraModelInput, OAI.PolycyclicRecognition.GeodesicMetricExistenceInput, OAI.PolycyclicRecognition.MatrixLieDifferentialInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.ProperChainMetric