CartanMeasuredConeCells.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Positive compact probability cells for the actual cone models

def OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone.withQuotientHaar line 25
Source documentation
Replacing only the quotient Haar normalization leaves the intrinsic kernel measure and its conjugation invariance intact.
```
def MeasuredCone.withQuotientHaar (μQ : Measure D.Q.carrier) (hμQ : μQ.IsHaarMeasure) :
    M.MeasuredCone F C where
…
```

theorem OAI.PolycyclicRecognition.compact_product_cell_probability_data line 40

Source documentation

The original compact product cell supports the inner-regular probability law used for concentration, with its unaltered product normalization.

theorem compact_product_cell_probability_data
    {Q K : Type*} [TopologicalSpace Q] [TopologicalSpace K]
    [PseudoMetrizableSpace Q] [PseudoMetrizableSpace K]
    [MeasurableSpace Q] [MeasurableSpace K] [BorelSpace Q] [BorelSpace K]
    [SecondCountableTopology Q] [SecondCountableTopology K]
    (μQ : Measure Q) (μK : Measure K) [SFinite μQ] [SFinite μK]
    (Z : Set Q) (J : Set K) (hZ : IsCompact Z) (hJ : IsCompact J)
    (hZ0 : μQ Z ≠ 0) (hZt : μQ Z ≠ ⊤) (hJ0 : μK J ≠ 0) (hJt : μK J ≠ ⊤) :
    (μQ.prod μK) (Z ×ˢ J) ≠ 0 ∧ (μQ.prod μK) (Z ×ˢ J) ≠ ⊤ ∧
      Nonempty (Z ×ˢ J) ∧
      ∀ ν : ProbabilityMeasure (Z ×ˢ J), (ν : Measure (Z ×ˢ J)).InnerRegular := by
…