LeanMachineLearning exposition

ProbabilityTheory.Kernel.symm_IicSuccProd🔗

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

symm_IicSuccProd🔗

LemmaProbabilityTheory.Kernel.symm_IicSuccProd
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.symm_IicSuccProd.{u_2} {X : ℕ → Type u_2}
  [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) :
  MeasurableEquiv.symm (MeasurableEquiv.IicSuccProd X n) =
    MeasurableEquiv.trans
      (MeasurableEquiv.prodCongr
        (MeasurableEquiv.refl ((i : ↥(Finset.Iic n)) → X ↑i))
        (MeasurableEquiv.piSingleton n))
      (MeasurableEquiv.IicProdIoc ⋯)
ProbabilityTheory.Kernel.symm_IicSuccProd.{u_2}
  {X : ℕ → Type u_2}
  [(n : ℕ) → MeasurableSpace (X n)]
  (n : ℕ) :
  MeasurableEquiv.symm
      (MeasurableEquiv.IicSuccProd X n) =
    MeasurableEquiv.trans
      (MeasurableEquiv.prodCongr
        (MeasurableEquiv.refl
          ((i : ↥(Finset.Iic n)) → X ↑i))
        (MeasurableEquiv.piSingleton n))
      (MeasurableEquiv.IicProdIoc ⋯)

Code

lemma symm_IicSuccProd (n : ℕ) :
    (MeasurableEquiv.IicSuccProd X n).symm =
      (MeasurableEquiv.prodCongr (MeasurableEquiv.refl _) (MeasurableEquiv.piSingleton n)).trans
        (MeasurableEquiv.IicProdIoc (Nat.le_succ n))
Type uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
rfl

Dependency graph

Type dependencies (1)

IicSuccProd🔗

DefinitionMeasurableEquiv.IicSuccProd
Details

Measurable equivalence between a product up to n + 1 and the pair of the product up to n and the space at n + 1.

🔗def
MeasurableEquiv.IicSuccProd.{u_3} (X : ℕ → Type u_3)
  [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) :
  ((i : ↥(Finset.Iic (n + 1))) → X ↑i) ≃ᵐ
    ((i : ↥(Finset.Iic n)) → X ↑i) × X (n + 1)
MeasurableEquiv.IicSuccProd.{u_3}
  (X : ℕ → Type u_3)
  [(n : ℕ) → MeasurableSpace (X n)]
  (n : ℕ) :
  ((i : ↥(Finset.Iic (n + 1))) → X ↑i) ≃ᵐ
    ((i : ↥(Finset.Iic n)) → X ↑i) ×
      X (n + 1)

Code

def _root_.MeasurableEquiv.IicSuccProd (X : ℕ → Type*) [∀ n, MeasurableSpace (X n)] (n : ℕ) :
    MeasurableEquiv (Π i : Iic (n + 1), X i) ((Π i : Iic n, X i) × X (n + 1)) :=
  (MeasurableEquiv.IicProdIoc (Nat.le_succ n)).symm.trans
    (MeasurableEquiv.prodCongr (MeasurableEquiv.refl _) (MeasurableEquiv.piSingleton n).symm)
Used by (11)

Actions: Source · Open Issue