OAI/Combinatorics/SharpThreshold/BlockSymmetry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem313.pasteCube line 12

   Source documentation

   Assemble a configuration on a coordinate subset and its complement.

   def pasteCube {α : Type u} {β : Type v} (P : α → Prop) [DecidablePred P]
       (x : {i // P i} → β) (y : {i // ¬ P i} → β) : α → β :=
   …

2. theorem OAI.Problem313.pasteCube_of_pos line 17
3. theorem OAI.Problem313.pasteCube_of_neg line 23
4. theorem OAI.Problem313.pasteCube_reindex line 30

   Source documentation

   A permutation preserving the free coordinates and fixing all exterior coordinates commutes with pasting, without changing the fixed exterior configuration.

   theorem pasteCube_reindex {α : Type u} {β : Type v} (P : α → Prop) [DecidablePred P]
       (π : Equiv.Perm α) (hP : ∀ i, P i ↔ P (π i))
       (hfix : ∀ i, ¬ P i → π i = i)
       (x : {i // P i} → β) (y : {i // ¬ P i} → β) :
       (fun i => pasteCube P x y (π.symm i)) =
         pasteCube P (fun i => x ((π.subtypeEquiv hP).symm i)) y := by
   …

   Mentions: OAI.Problem313.pasteCube

5. def OAI.Problem313.restrictCube line 45

   Source documentation

   Restriction of a function to a coordinate subset, with exterior values fixed.

   def restrictCube {α : Type u} {β : Type v} {γ : Type w} (P : α → Prop) [DecidablePred P]
       (f : (α → β) → γ) (y : {i // ¬ P i} → β) : ({i // P i} → β) → γ :=
   …

6. theorem OAI.Problem313.restrictCube_invariant line 51

   Source documentation

   Coordinate symmetry survives conditioning outside a set when the symmetry fixes every exterior coordinate individually.

   theorem restrictCube_invariant {α : Type u} {β : Type v} {γ : Type w} (P : α → Prop) [DecidablePred P]
       (π : Equiv.Perm α) (hP : ∀ i, P i ↔ P (π i))
       (hfix : ∀ i, ¬ P i → π i = i) (f : (α → β) → γ)
       (hf : ∀ z, f (fun i => z (π.symm i)) = f z)
       (x : {i // P i} → β) (y : {i // ¬ P i} → β) :
       restrictCube P f y (fun i => x ((π.subtypeEquiv hP).symm i)) =
         restrictCube P f y x := by
   …

   Mentions: OAI.Problem313.restrictCube