OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanActualProbeProfiles.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.CartanFactorModel.profileChart line 22

   Source documentation

   A Cartan chart, in the coordinates used for the profiles.

   def CartanFactorModel.profileChart
       (bD : Basis (Fin (finrank ℝ H)) ℝ H) : (Fin (finrank ℝ H) → ℝ) → G :=
   …

2. theorem OAI.PolycyclicRecognition.CartanFactorModel.continuous_profileChart line 27
3. def OAI.PolycyclicRecognition.CartanFactorModel.sampledProbeSuffix line 34

   Source documentation

   The original sample is multiplied by the actual probe prefix.

   def CartanFactorModel.sampledProbeSuffix
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (y : Fin (finrank ℝ (cartanRootIdeal H)) → ℝ) (v : cartanRootIdeal H) : G :=
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

4. def OAI.PolycyclicRecognition.CartanFactorModel.sampledProbeProfile line 42

   Source documentation

   This is a continuous map on the whole Cartan chart, before restricting to the compact set chosen for all three paths.

   def CartanFactorModel.sampledProbeProfile
       (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)
       (y : Fin (finrank ℝ (cartanRootIdeal H)) → ℝ) (v : cartanRootIdeal H) :
       C((Fin (finrank ℝ H) → ℝ), W) :=
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

5. theorem OAI.PolycyclicRecognition.CartanFactorModel.sampledProbeProfile_apply line 51
6. theorem OAI.PolycyclicRecognition.CartanFactorModel.measurable_sampledProbeProfile line 71

   Source documentation

   A Borel logarithmic prefix, including a tile-selected anchor, gives a Borel actual profile under the independent product sampling law.

   theorem CartanFactorModel.measurable_sampledProbeProfile
       (hN : Continuous F.ExpN) (hD : Continuous F.ExpD)
       (J : G → W) (hJ : Continuous J) (x : G) (r : ℝ)
       (b₀ bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (bD : Basis (Fin (finrank ℝ H)) ℝ H)
       {Y : Type*} [MeasurableSpace Y] (v : Y → cartanRootIdeal H)
       (hv : Measurable (fun y => b₀.equivFun (v y))) :
       Measurable (fun p : (Fin (finrank ℝ (cartanRootIdeal H)) → ℝ) × Y =>
         F.sampledProbeProfile hD J hJ x r bN bD p.1 (v p.2)) := by
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

7. theorem OAI.PolycyclicRecognition.CartanFactorModel.sampledProbeProfile_eq_of_exp_eq line 104

   Source documentation

   The initial and final profiles agree exactly when the actual group suffixes agree. In particular this identifies the third chain's initial profile with the second chain's terminal anchor.

   theorem CartanFactorModel.sampledProbeProfile_eq_of_exp_eq
       (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)
       (y : Fin (finrank ℝ (cartanRootIdeal H)) → ℝ) (u v : cartanRootIdeal H)
       (h : F.ExpN (F.N.equiv u) = F.ExpN (F.N.equiv v)) :
       F.sampledProbeProfile hD J hJ x r bN bD y u =
         F.sampledProbeProfile hD J hJ x r bN bD y v := by
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal