CartanSampledProbeFrames.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The original center and exact group frames of a sampled profile

def OAI.PolycyclicRecognition.CartanFactorModel.sampleRoot line 21
Source documentation
The root element selected by the independent coordinate-cube sample.
```
def CartanFactorModel.sampleRoot
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (y : Fin (finrank ℝ (cartanRootIdeal H)) → ℝ) : F.N.carrier :=
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanFactorModel.sampledProbeSuffix_eq line 28

Source documentation

An endpoint identity can be used without changing the profile center.

theorem CartanFactorModel.sampledProbeSuffix_eq
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (y : Fin (finrank ℝ (cartanRootIdeal H)) → ℝ) (v : cartanRootIdeal H)
    (u : F.N.carrier) (hu : F.ExpN (F.N.equiv v) = u) :
    F.sampledProbeSuffix bN y v = F.inclusionN (F.sampleRoot bN y * u) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanFactorModel.sampledProbeSuffix_eq_root line 37

Source documentation

The endpoint in exponential coordinates and its group-valued frame agree.

theorem CartanFactorModel.sampledProbeSuffix_eq_root
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (y : Fin (finrank ℝ (cartanRootIdeal H)) → ℝ) (v : cartanRootIdeal H) :
    F.sampledProbeSuffix bN y v =
      F.inclusionN (F.sampleRoot bN y * F.ExpN (F.N.equiv v)) :=
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanFactorModel.sampledProbeProfile_eq line 46

Source documentation

Restricting the chart does not re-center a sampled profile. This is the identity needed by the source count, including the original subtracted value.

theorem CartanFactorModel.sampledProbeProfile_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)) → ℝ) (v : cartanRootIdeal H)
    (u : F.N.carrier) (hu : F.ExpN (F.N.equiv v) = u)
    {Z : Set (Fin (finrank ℝ H) → ℝ)} (z : Z) :
    F.sampledProbeProfile hD J hJ x r bN bD y v z =
      rescaledMapProfile J x (F.inclusionN (F.sampleRoot bN y * u)) r
        (fun z : Z => F.profileChart bD z.val) z := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.rescaledMapProfile

theorem OAI.PolycyclicRecognition.CartanFactorModel.profileChart_coordinates line 64
Source documentation
The chart point corresponding to a physical Cartan vector is exact even when the logarithmic rescaling basis moves with the scale.
```
theorem CartanFactorModel.profileChart_coordinates
    (bD : Basis (Fin (finrank ℝ H)) ℝ H) (v : H) :
    F.profileChart bD (bD.equivFun v) = F.inclusionD (F.ExpD (F.D.equiv v)) := by
…
```