CartanTransformedPolarTemplates.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The actual target templates in the offset comparison

The target cone is the inverse image under precomposition by the affine label. Its vanishing widths and positive ideal widths are consequences of the source polar template, without requiring the label to preserve a ball.

def OAI.PolycyclicRecognition.transformedPolarCone line 22
Source documentation
The target functionals whose pullbacks lie in the source cone.
```
def transformedPolarCone (K : ProperCone ℝ (StrongDual ℝ W)) (A : W ≃ₗ[ℝ] W) :
    ProperCone ℝ (StrongDual ℝ W) :=
…
```
theorem OAI.PolycyclicRecognition.mem_transformedPolarCone line 27

theorem OAI.PolycyclicRecognition.transformedPolar_width line 33

Source documentation

The exact support width of a transformed and dilated polar template.

theorem transformedPolar_width (K : ProperCone ℝ (StrongDual ℝ W))
    (A : W ≃ₗ[ℝ] W) (β : StrongDual ℝ W) {c : ℝ} (hc : 0 ≤ c) :
    sSup (β '' (A '' ((fun x : W => c • x) '' conePolarTemplate K))) =
      c * conePolarWidth K (β.comp A.toLinearMap.toContinuousLinearMap) := by
…

Mentions: OAI.PolycyclicRecognition.conePolarTemplate, OAI.PolycyclicRecognition.conePolarWidth

theorem OAI.PolycyclicRecognition.CartanWordModel.weightSupport_transformed_polar line 54
theorem OAI.PolycyclicRecognition.CartanWordModel.transformed_polar_width_properties line 66
Source documentation
Both target path templates have zero quotient widths and strictly positive widths outside the pulled-back cone.
```
theorem transformed_polar_width_properties (K : ProperCone ℝ (StrongDual ℝ W))
    (A : W ≃ₗ[ℝ] W) {c : ℝ} (hc : 0 < c) :
    let E := A '' ((fun x : W => c • x) '' conePolarTemplate K)
…
```
Mentions: OAI.PolycyclicRecognition.conePolarTemplate

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_transformed_polar_probe_basis line 101

Source documentation

One target ideal basis maximizes every radius used by the path comparison.

theorem exists_transformed_polar_probe_basis (K : ProperCone ℝ (StrongDual ℝ W))
    (A : W ≃ₗ[ℝ] W)
    (bI : Basis (Fin (finrank ℝ
      (M.coneWordIdeal (heightConePreimage T eW (transformedPolarCone K A)))) )
      ℝ (M.coneWordIdeal (heightConePreimage T eW (transformedPolarCone K A)))) :
    ∃ β : M.ConeIdealBases (heightConePreimage T eW (transformedPolarCone K A)),
      ∀ c : ℝ, 0 ≤ c →
        M.IsMaximizingConeIdealBasis (heightConePreimage T eW (transformedPolarCone K A)) bI
          ((M.supportIn T hunimod eW).weightSupport
            (A '' ((fun x : W => c • x) '' conePolarTemplate K))) β := by
…

Mentions: OAI.PolycyclicRecognition.CartanWordModel.heightConePreimage, OAI.PolycyclicRecognition.transformedPolarCone, OAI.PolycyclicRecognition.conePolarTemplate

theorem OAI.PolycyclicRecognition.CartanWordModel.transformed_polar_ideal_exponent line 127

Source documentation

The target ideal volume exponent equals the original polar-template exponent under an actual template-symmetry label.

theorem transformed_polar_ideal_exponent (K : ProperCone ℝ (StrongDual ℝ W))
    (A : templateSymmetryGroup (M.supportIn T hunimod eW))
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (bI : Basis (Fin (finrank ℝ
      (M.coneWordIdeal (heightConePreimage T eW (transformedPolarCone K A.val)))))
      ℝ (M.coneWordIdeal (heightConePreimage T eW (transformedPolarCone K A.val))))
    {c : ℝ} (hc : 0 < c)
    (β : M.ConeIdealBases (heightConePreimage T eW (transformedPolarCone K A.val)))
    (hβ : M.IsMaximizingConeIdealBasis
      (heightConePreimage T eW (transformedPolarCone K A.val)) bI
      ((M.supportIn T hunimod eW).weightSupport
        (A.val '' ((fun x : W => c • x) '' conePolarTemplate K))) β) :
…

Mentions: OAI.PolycyclicRecognition.templateSymmetryGroup, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.CartanWordModel.heightConePreimage, OAI.PolycyclicRecognition.transformedPolarCone, OAI.PolycyclicRecognition.conePolarTemplate