CartanPolarProbeTemplates.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Actual polar-template widths for the three probe boxes

def OAI.PolycyclicRecognition.CartanWordModel.heightConePreimage line 22
Source documentation
Pull a cone of height functionals back to the actual Cartan weights.
```
def heightConePreimage (K : ProperCone ℝ (StrongDual ℝ W)) : Set (H →ₗ[ℝ] ℝ) :=
…
```
def OAI.PolycyclicRecognition.CartanWordModel.polarProbeWidths line 25
theorem OAI.PolycyclicRecognition.CartanWordModel.weight_mem_heightConePreimage_iff line 28

theorem OAI.PolycyclicRecognition.CartanWordModel.weightSupport_polar_smul line 35

Source documentation

The support exponents of the normalized probe templates are exactly the polar widths multiplied by their radii.

theorem weightSupport_polar_smul (K : ProperCone ℝ (StrongDual ℝ W))
    {c : ℝ} (hc : 0 ≤ c) (i : Fin M.letterCount) :
    (M.supportIn T hunimod eW).weightSupport
      ((fun x : W => c • x) '' conePolarTemplate K) i =
      c * conePolarWidth K ((M.supportIn T hunimod eW).weight i).toContinuousLinearMap :=
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.polar_width_nonneg line 42
theorem OAI.PolycyclicRecognition.CartanWordModel.polar_width_zero line 47
theorem OAI.PolycyclicRecognition.CartanWordModel.polar_width_pos line 52
theorem OAI.PolycyclicRecognition.CartanWordModel.polar_probe_template_properties line 59
Source documentation
The normalized source templates satisfy every compactness, convexity and zero-width condition required by the actual three-chain construction.
```
theorem polar_probe_template_properties (K : ProperCone ℝ (StrongDual ℝ W))
    {c : ℝ} (hc : 0 ≤ c) :
    let E := (fun x : W => c • x) '' conePolarTemplate K
…
```
Mentions: OAI.PolycyclicRecognition.conePolarTemplate

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_polar_probe_basis line 81

Source documentation

One actual mixed-word basis maximizes every nonnegative multiple of the polar template, including all three radii in the strict-width tiling.

theorem exists_polar_probe_basis (K : ProperCone ℝ (StrongDual ℝ W))
    (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal (heightConePreimage T eW K))))
      ℝ (M.coneWordIdeal (heightConePreimage T eW K))) :
    ∃ β : M.ConeIdealBases (heightConePreimage T eW K),
      M.IsMaximizingConeIdealBasis (heightConePreimage T eW K) bI
        (fun i => conePolarWidth K
          ((M.supportIn T hunimod eW).weight i).toContinuousLinearMap) β ∧
      ∀ c : ℝ, 0 ≤ c → M.IsMaximizingConeIdealBasis (heightConePreimage T eW K) bI
        ((M.supportIn T hunimod eW).weightSupport
          ((fun x : W => c • x) '' conePolarTemplate K)) β := by
…

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