OAI/NumberTheory/DukePrimeDegree/Entropy/RootFactorConditionalProduct.lean
3 declarations, 0 contain sorry, 0 declared as axioms
The conditional product step for a noncommuting root factor
A measurable change of transverse coordinates preserves the real conditional. In a genuine root factor chart, the proved neutral holonomy then makes that conditional independent of the remaining root coordinates. This is the local step of EK2003, Proposition 8.3.
- lemma
OAI.DukePrimeDegree.factorChart_nested_conditionalsline 26 - lemma
OAI.DukePrimeDegree.factorChart_ae_nestedline 53 - theorem
OAI.DukePrimeDegree.rootFactorChart_real_conditionals_constantline 73