Documentation

KolmogorovExtension4.CompactSystem

def IsCompactSystem {α : Type u_1} (p : Set αProp) :

A set of sets is a compact system if, whenever a countable subfamily has empty intersection, then finitely many of them already have empty intersection.

Equations
Instances For
    noncomputable def IsCompactSystem.support {α : Type u_1} {p : Set αProp} {C : Set α} (hp : IsCompactSystem p) (hC : ∀ (i : ), p (C i)) (hC_empty : ⋂ (i : ), C i = ) :

    In a compact system, given a countable family with empty intersection, we choose a finite subfamily with empty intersection

    Equations
    • hp.support hC hC_empty = .choose
    Instances For
      theorem IsCompactSystem.iInter_eq_empty {α : Type u_1} {p : Set αProp} {C : Set α} (hp : IsCompactSystem p) (hC : ∀ (i : ), p (C i)) (hC_empty : ⋂ (i : ), C i = ) :
      ihp.support hC hC_empty, C i =

      We prove that the closedCompactCylinders are a compact system.

      def allProj {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) :
      Set ι

      All indices in ι that are constrained by the condition ∀ n, s n ∈ closedCompactCylinders α. That is, the union of all indices in the bases of the cylinders.

      Equations
      Instances For
        theorem subset_allProj {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (n : ) :
        theorem exists_nat_proj {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (i : ι) (hi : i allProj hs) :
        noncomputable def indexProj {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (i : (allProj hs)) :

        The smallest n such that i ∈ Js (hs n). That is, the first n such that i belongs to the finset defining the cylinder for s n.

        Equations
        Instances For
          theorem mem_indexProj {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (i : (allProj hs)) :
          theorem indexProj_le {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (n : ) (i : { x : ι // x closedCompactCylinders.finset }) :
          indexProj hs i, n
          theorem surjective_proj_allProj {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} [∀ (i : ι), Nonempty (α i)] (hs : ∀ (n : ), s n closedCompactCylinders α) :
          Function.Surjective fun (f : (i : ι) → α i) (i : (allProj hs)) => f i
          def projCylinder {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (n : ) :
          Set ((i : (allProj hs)) → α i)

          Given a countable family of closed cylinders, consider one of them as depending only on the countably many coordinates that appear in all of them.

          Equations
          Instances For
            theorem mem_projCylinder {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (n : ) (x : (i : (allProj hs)) → α i) :
            x projCylinder hs n (fun (i : { x : ι // x closedCompactCylinders.finset }) => x i, ) closedCompactCylinders.set
            theorem preimage_projCylinder {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (n : ) :
            (fun (f : (i : ι) → α i) (i : (allProj hs)) => f i) ⁻¹' projCylinder hs n = s n
            theorem nonempty_projCylinder {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (n : ) (hs_nonempty : (s n).Nonempty) :
            (projCylinder hs n).Nonempty
            theorem nonempty_projCylinder_iff {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} [∀ (i : ι), Nonempty (α i)] (hs : ∀ (n : ), s n closedCompactCylinders α) (n : ) :
            (projCylinder hs n).Nonempty (s n).Nonempty
            theorem isClosed_projCylinder {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (hs_closed : ∀ (n : ), IsClosed (closedCompactCylinders.set )) (n : ) :
            def piCylinderSet {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) :
            Set ((i : (allProj hs)) → α i)

            Given countably many closed compact cylinders, the product set which, in each relevant coordinate, is the projection of the first cylinder for which this coordinate is relevant.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem mem_piCylinderSet {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (x : (i : (allProj hs)) → α i) :
              x piCylinderSet hs ∀ (i : (allProj hs)), x i (fun (a : (j : { x : ι // x closedCompactCylinders.finset }) → α j) => a i, ) '' closedCompactCylinders.set
              theorem isCompact_piCylinderSet {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) :
              theorem piCylinderSet_eq_pi_univ {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) :
              piCylinderSet hs = Set.univ.pi fun (i : (allProj hs)) => (fun (a : (j : { x : ι // x closedCompactCylinders.finset }) → α j) => a i, ) '' closedCompactCylinders.set
              theorem isClosed_piCylinderSet {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) :
              theorem nonempty_piCylinderSet {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (hs_nonempty : ∀ (i : ), (s i).Nonempty) :
              (piCylinderSet hs).Nonempty
              theorem iInter_subset_piCylinderSet {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) :
              ⋂ (n : ), projCylinder hs n piCylinderSet hs
              theorem nonempty_iInter_projCylinder_inter_piCylinderSet {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (hs_nonempty : ∀ (i : ), (s i).Nonempty) (h_nonempty : ∀ (n : ), (⋂ (i : ), ⋂ (_ : i n), projCylinder hs i).Nonempty) (n : ) :
              ((⋂ (i : ), ⋂ (_ : i n), projCylinder hs i) piCylinderSet hs).Nonempty
              theorem nonempty_iInter_projCylinder {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} (hs : ∀ (n : ), s n closedCompactCylinders α) (hs_nonempty : ∀ (i : ), (s i).Nonempty) (h_nonempty : ∀ (n : ), (⋂ (i : ), ⋂ (_ : i n), projCylinder hs i).Nonempty) :
              (⋂ (i : ), projCylinder hs i).Nonempty
              theorem exists_finset_iInter_projCylinder_eq_empty {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] {s : Set ((i : ι) → α i)} [∀ (i : ι), Nonempty (α i)] (hs : ∀ (n : ), s n closedCompactCylinders α) (h : ⋂ (n : ), projCylinder hs n = ) :
              ∃ (t : Finset ), it, projCylinder hs i =
              theorem isCompactSystem_closedCompactCylinders {ι : Type u_1} {α : ιType u_2} [(i : ι) → TopologicalSpace (α i)] :

              The closedCompactCylinders are a compact system.