OAI/Analysis/FiniteFactor/CrossedProduct/ResamplingLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceResampling_coordinate_compProd line 10
2. theorem OAI.FiniteFactor.sourceResampling_compProd_eq_map line 24

   Source documentation

   Each replacement pattern is exactly the unrestricted source pair law.

   theorem sourceResampling_compProd_eq_map (I : Finset SourceCoordinate) :
       sourceSamplingHaar ⊗ₘ sourceResamplingKernel I =
         sourceSamplingPairHaar.map (sourceSamplingLimitMap I) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.sourceResamplingKernel, OAI.FiniteFactor.sourceSamplingLimitMap