OAI/Analysis/FiniteFactor/Coupling/BlockLimit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.CouplingParameters.BlockCoordinate line 13

   Source documentation

   The source coordinates, retaining the block and the position in that block.

   Also declared: ComparatorChallenges/ProductBrown.lean:427 (same declaration text).

   abbrev BlockCoordinate (m : ℕ → ℕ) := Σ s : ℕ, Fin (m s)

2. def OAI.FiniteFactor.CouplingParameters.blockPrefix line 15
3. theorem OAI.FiniteFactor.CouplingParameters.mem_blockPrefix line 18
4. theorem OAI.FiniteFactor.CouplingParameters.blockPrefix_mono line 21
5. theorem OAI.FiniteFactor.CouplingParameters.blockPrefix_cover line 25
6. theorem OAI.FiniteFactor.CouplingParameters.blockPrefix_energy line 30
7. theorem OAI.FiniteFactor.CouplingParameters.infinite_block_source_density line 52
8. def OAI.FiniteFactor.CouplingParameters.blockProductCoupling line 71

   Source documentation

   Actual augmented law on the block-indexed coordinates.

   def blockProductCoupling (p : ℕ → CouplingParameters) (m : ℕ → ℕ) :
       Measure (BlockCoordinate m → Fin 6 × (ℝ × ℝ)) :=
   …

   Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.BlockCoordinate

9. instance OAI.FiniteFactor.CouplingParameters.blockProductCoupling_probability line 75
10. def OAI.FiniteFactor.CouplingParameters.blockProductEndpoint line 78
11. theorem OAI.FiniteFactor.CouplingParameters.blockProductEndpoint_law line 82
12. theorem OAI.FiniteFactor.CouplingParameters.blockProductEndpoint_L2_density line 94

    Source documentation

    The density belongs to the actual law of the selected endpoint map, rather than only to an abstract measure with matching finite moments.

    theorem blockProductEndpoint_L2_density (p : ℕ → CouplingParameters) (m : ℕ → ℕ)
        (hm : ∀ s, (p s).m = (m s : ℝ)) (j : ℕ)
        (htag : ∀ s, (p s).tagged = decide (s=j))
        (hκ : ∀ s, (p s).kappa = sourceKappa s) (right : BlockCoordinate m → Bool) :
        ∃ g : (BlockCoordinate m → ℝ) → ℝ,
          MemLp g 2 (Measure.infinitePi (fun _ : BlockCoordinate m => unitIntervalMeasure)) ∧
          (∀ᵐ x ∂Measure.infinitePi (fun _ : BlockCoordinate m => unitIntervalMeasure), 0 ≤ g x) ∧
          (∫ x, g x ^ 2 ∂Measure.infinitePi (fun _ : BlockCoordinate m => unitIntervalMeasure)) ≤
            Real.exp (20*(2*(∑' s, sourceKappa s ^ 2)+1)) ∧
          (blockProductCoupling p m).map (blockProductEndpoint right) =
            (Measure.infinitePi (fun _ : BlockCoordinate m => unitIntervalMeasure)).withDensity
              (fun x => ENNReal.ofReal (g x)) := by
    …

    Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.sourceKappa, OAI.FiniteFactor.CouplingParameters.BlockCoordinate, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.CouplingParameters.blockProductCoupling, OAI.FiniteFactor.CouplingParameters.blockProductEndpoint