LevelIndependence.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.equalLevelEquiv line 14

theorem OAI.ExactQuantumFactoring.equalLevel_card line 23

Source documentation

Counting the equality of two independent levels by fibers, with no assumption about an approximately uniform distribution.

theorem equalLevel_card {A B T : Type*} [Fintype A] [Fintype B]
    (f : A → T) (g : B → T) [DecidableEq T] :
    Fintype.card {x : A × B // f x.1 = g x.2} = ∑ b : B, Fintype.card {a : A // f a = g b} := by
…

theorem OAI.ExactQuantumFactoring.twice_equalLevel_card_le line 29
def OAI.ExactQuantumFactoring.allEqualLevelEquiv line 39

theorem OAI.ExactQuantumFactoring.allEqualLevel_card line 61

Source documentation

Exact product formula used in the source's retrospective F computation.

theorem allEqualLevel_card {ι T : Type*} {G : ι → Type*} [Fintype ι] [Fintype T]
    [∀ i, Fintype (G i)] [DecidableEq T] [DecidableEq ι] (i₀ : ι) (f : ∀ i, G i → T) :
    Fintype.card {x : ∀ i, G i // ∀ i, f i (x i) = f i₀ (x i₀)} =
      ∑ t : T, ∏ i : ι, Fintype.card {x : G i // f i x = t} := by
…

theorem OAI.ExactQuantumFactoring.twice_constrained_card_le line 72

Source documentation

Extra components can only decrease the all-equal event.

theorem twice_constrained_card_le {A B C T : Type*} [Fintype A] [Fintype B] [Fintype C]
    (f : A → T) (g : B → T) [DecidableEq T]
    (P : A × B × C → Prop) [DecidablePred P]
    (hp : ∀ x, P x → f x.1 = g x.2.1)
    (hf : ∀ t, 2 * Fintype.card {a : A // f a = t} ≤ Fintype.card A) :
    2 * Fintype.card {x : A × B × C // P x} ≤
      Fintype.card A * Fintype.card B * Fintype.card C := by
…

theorem OAI.ExactQuantumFactoring.twice_allEqualLevel_card_le line 98

Source documentation

Two distinct independent components suffice for the exact half bound.

theorem twice_allEqualLevel_card_le {ι T : Type*} {G : ι → Type*}
    [Fintype ι] [∀ i, Fintype (G i)] [DecidableEq T] [DecidableEq ι]
    (i₀ i₁ : ι) (hi : i₁ ≠ i₀) (f : ∀ i, G i → T)
    (hf : ∀ t, 2 * Fintype.card {a : G i₀ // f i₀ a = t} ≤ Fintype.card (G i₀)) :
    2 * Fintype.card {x : ∀ i, G i // ∀ i, f i (x i) = f i₀ (x i₀)} ≤
      Fintype.card (∀ i, G i) := by
…