Functionality

Difficulty: moderate — 1 definitions, 1 abbreviations, 0 lemmas, 4 theorems, 0 examples.

definition abbreviation theorem
legend
theorem BitFunction.cardinality (n m : ℕ) : Fintype.card (BitFunction n m) = 2 ^ (m * 2 ^ n)
Show details 
fun n m =>
  Eq.mpr (id (congrArg (fun _a => _a = 2 ^ (m * 2 ^ n)) Fintype.card_fun))
    (Eq.mpr
      (id
        (congrArg (fun _a => _a ^ Fintype.card (Fin n → Bit) = 2 ^ (m * 2 ^ n))
          (BitSequence.cardinality m)))
      (Eq.mpr (id (congrArg (fun _a => (2 ^ m) ^ _a = 2 ^ (m * 2 ^ n)) (BitSequence.cardinality n)))
        (Eq.mpr (id (congrArg (fun _a => _a = 2 ^ (m * 2 ^ n)) (Eq.symm (pow_mul 2 m (2 ^ n)))))
          (Eq.mpr (id (congrArg (fun _a => 2 ^ _a = 2 ^ _a) (Nat.mul_comm m (2 ^ n))))
            (Eq.refl (2 ^ (2 ^ n * m)))))))

Complexity: 5463 (size of the value term)

Dependencies: Bit, BitFunction

Proof dependencies: BitSequence, BitSequence.cardinality

Mathlib dependencies: Fintype.card, Fintype.card_fun, pow_mul

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Fin, Nat, Nat.mul_comm, congrArg, id

Used by: BitFunction.cardinality_input_growth, BitFunction.cardinality_output_growth

theorem BitFunction.cardinality_output_growth (n m : ℕ) :
  Fintype.card (BitFunction n (m + 1)) = Fintype.card (BitFunction n m) * 2 ^ 2 ^ n
Show details 
fun n m =>
  Eq.mpr
    (id
      (congrArg (fun _a => _a = Fintype.card (BitFunction n m) * 2 ^ 2 ^ n)
        (BitFunction.cardinality n (m + 1))))
    (Eq.mpr
      (id
        (congrArg (fun _a => 2 ^ ((m + 1) * 2 ^ n) = _a * 2 ^ 2 ^ n) (BitFunction.cardinality n m)))
      (Eq.mpr
        (id (congrArg (fun _a => 2 ^ _a = 2 ^ (m * 2 ^ n) * 2 ^ 2 ^ n) (add_one_mul m (2 ^ n))))
        (Eq.mpr
          (id
            (congrArg (fun _a => _a = 2 ^ (m * 2 ^ n) * 2 ^ 2 ^ n) (pow_add 2 (m * 2 ^ n) (2 ^ n))))
          (Eq.refl (2 ^ (m * 2 ^ n) * 2 ^ 2 ^ n)))))

Complexity: 7843 (size of the value term)

Dependencies: Bit, BitFunction

Proof dependencies: BitFunction.cardinality

Mathlib dependencies: Fintype.card, add_one_mul, pow_add

Lean core dependencies: Eq, Eq.mpr, Fin, Nat, congrArg, id

Used by: (none)

theorem BitFunction.cardinality_input_growth (n m : ℕ) :
  Fintype.card (BitFunction (n + 1) m) = Fintype.card (BitFunction n m) ^ 2
Show details 
fun n m =>
  Eq.mpr
    (id
      (congrArg (fun _a => _a = Fintype.card (BitFunction n m) ^ 2)
        (BitFunction.cardinality (n + 1) m)))
    (Eq.mpr (id (congrArg (fun _a => 2 ^ (m * 2 ^ (n + 1)) = _a ^ 2) (BitFunction.cardinality n m)))
      (Eq.mpr (id (congrArg (fun _a => 2 ^ (m * _a) = (2 ^ (m * 2 ^ n)) ^ 2) (pow_succ 2 n)))
        (Eq.mpr
          (id
            (congrArg (fun _a => 2 ^ _a = (2 ^ (m * 2 ^ n)) ^ 2)
              (Eq.symm (Nat.mul_assoc m (2 ^ n) 2))))
          (Eq.mpr (id (congrArg (fun _a => _a = (2 ^ (m * 2 ^ n)) ^ 2) (pow_mul 2 (m * 2 ^ n) 2)))
            (Eq.refl ((2 ^ (m * 2 ^ n)) ^ 2))))))

Complexity: 8363 (size of the value term)

Dependencies: Bit, BitFunction

Proof dependencies: BitFunction.cardinality

Mathlib dependencies: Fintype.card, pow_mul, pow_succ

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Fin, Nat, Nat.mul_assoc, congrArg, id

Used by: (none)

def BitFunction.comp {n m p : ℕ} (f : BitFunction n m) (g : BitFunction m p) : BitFunction n p
Show details 
| f.comp g = g ∘ f

Complexity: 41 (size of the value term)

Outer dependencies: BitFunction

Inner dependencies: Bit

Lean core dependencies: Fin, Function.comp, Nat

Used by: BitFunction.comp_assoc

theorem BitFunction.comp_assoc {n m p q : ℕ} (f : BitFunction n m) (g : BitFunction m p)
  (h : BitFunction p q) : (f.comp g).comp h = f.comp (g.comp h)
Show details 
fun {n m p q} f g h => rfl

Complexity: 55 (size of the value term)

Dependencies: BitFunction, BitFunction.comp

Lean core dependencies: Eq, Nat, rfl

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionabbreviationtheoremdeclared elsewheredependencyproof dependency
legend