OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCanonicalProfiles.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual profiles indexed by a real physical scale

  1. def OAI.PolycyclicRecognition.CartanFactorModel.realScaleProfile line 22
  2. theorem OAI.PolycyclicRecognition.CartanFactorModel.realScaleProfile_apply line 31
  3. theorem OAI.PolycyclicRecognition.CartanFactorModel.realScaleProfile_mean_norm_le line 41

    Source documentation

    A normalized suffix bound gives the same bound on the mean offset.

    theorem CartanFactorModel.realScaleProfile_mean_norm_le
    [IsIsometricSMul G G]
    (hD : Continuous F.ExpD) (J : G → W) {K : ℝ≥0} (hJ : LipschitzWith K J) (x : G)
    (X : I → H) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    {r C : ℝ} (hr : 1 ≤ r) (μ : ProbabilityMeasure F.N.carrier)
    (hbound : ∀ᵐ k ∂(μ : Measure F.N.carrier), dist 1 (F.inclusionN k) / r ≤ C) :
    ‖∫ k, F.realScaleProfile hD J hJ.continuous x X S β r k 0
      ∂(μ : Measure F.N.carrier)‖ ≤ (K : ℝ) * C := by
…

    Mentions: OAI.PolycyclicRecognition.WordBasisSelections