CartanFixedProfileMeasurable.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual measurable profiles of the sampled probe chains

theorem OAI.PolycyclicRecognition.CartanFactorModel.measurable_fixed_sampledProbeProfile line 22

Source documentation

The fixed initial suffix is a continuous function of the original sample. This proof avoids introducing an artificial product probe space.

theorem CartanFactorModel.measurable_fixed_sampledProbeProfile
    (hN : Continuous F.ExpN) (hD : Continuous F.ExpD)
    (J : G → W) (hJ : Continuous J) (x : G) (r : ℝ)
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (bD : Basis (Fin (finrank ℝ H)) ℝ H) (v : cartanRootIdeal H)
    (Z : Set (Fin (finrank ℝ H) → ℝ))
    [MeasurableSpace C(Z, W)] [BorelSpace C(Z, W)] :
    Measurable (fun y : Fin (finrank ℝ (cartanRootIdeal H)) → ℝ =>
      (F.sampledProbeProfile hD J hJ x r bN bD y v).restrict Z) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal