`independent`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.RSCoupledAxis
domain: Foundation
line: 39 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.RSCoupledAxis on GitHub at line 39.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  36  primitive : RSPrimitive
  37
  38/-- RS-independence means the axes are carried by different primitives. -/
  39def independent {n m : ℕ} (A : CoupledAxis n) (B : CoupledAxis m) : Prop :=
  40  A.primitive ≠ B.primitive
  41
  42/-- Pairwise independent triple of same-size axes. -/
  43structure RSIndependentTriple (n : ℕ) where
  44  axis1 : CoupledAxis n
  45  axis2 : CoupledAxis n
  46  axis3 : CoupledAxis n
  47  indep12 : independent axis1 axis2
  48  indep13 : independent axis1 axis3
  49  indep23 : independent axis2 axis3
  50
  51/-- Pairwise independent disjoint sum of same-size axes. -/
  52structure RSDisjointSum3 (n : ℕ) where
  53  axis1 : CoupledAxis n
  54  axis2 : CoupledAxis n
  55  axis3 : CoupledAxis n
  56  indep12 : independent axis1 axis2
  57  indep13 : independent axis1 axis3
  58  indep23 : independent axis2 axis3
  59
  60/-- Product of the cardinalities of three same-size RS-independent axes. -/
  61def tripleProductCard {n : ℕ} (T : RSIndependentTriple n) : ℕ :=
  62  @Fintype.card T.axis1.Ix T.axis1.finite *
  63    @Fintype.card T.axis2.Ix T.axis2.finite *
  64    @Fintype.card T.axis3.Ix T.axis3.finite
  65
  66/-- The tensor-product count of three same-size RS-independent axes is n^3. -/
  67theorem triple_card {n : ℕ} (T : RSIndependentTriple n) :
  68    tripleProductCard T = n * n * n := by
  69  unfold tripleProductCard

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.