Documentation

Verification.ApproximationExamples

← Mathematical handbook
source
noncomputable def Verification.ApproximationExamples.lowerMatrix :
ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 4 ⋯)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Verification.ApproximationExamples.coarseMatrix :
    ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Verification.ApproximationExamples.upperMatrix :
      ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 4 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 4 ⋯)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Verification.ApproximationExamples.shuffleMatrix :
        ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 4 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 4 ⋯)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Verification.ApproximationExamples.lowerMatrix_xi :
          lowerMatrix.checkerboard.chatterjeeXi = 1 / 16
          source
          theorem Verification.ApproximationExamples.coarseMatrix_xi :
          coarseMatrix.checkerboard.chatterjeeXi = 1 / 8
          source
          theorem Verification.ApproximationExamples.upperMatrix_xi :
          upperMatrix.checkerboard.chatterjeeXi = 5 / 8
          source
          theorem Verification.ApproximationExamples.coarseMatrix_checkMin_xi :
          coarseMatrix.checkMin.chatterjeeXi = 7 / 16
          source
          theorem Verification.ApproximationExamples.shuffleMatrix_checkMin_xi :
          shuffleMatrix.checkMin.chatterjeeXi = 1
          source
          theorem Verification.ApproximationExamples.upperMatrix_mtp2 :
          upperMatrix.checkerboard.HasMTP2Density
          source
          theorem Verification.ApproximationExamples.uniform_four_coord_two_point (i : Fin 4) (j : Fin 3) :
          (ProbabilityTheory.Copula.IntervalPartition.uniform 4 ⋯).coord i ((ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯).point j) = if ↑i < 2 * ↑j then 1 else 0
          source
          theorem Verification.ApproximationExamples.lowerMatrix_coarsen (i j : Fin 2) :
          (lowerMatrix.checkerboard.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).mass i j = coarseMatrix.mass i j
          source
          theorem Verification.ApproximationExamples.upperMatrix_coarsen (i j : Fin 2) :
          (upperMatrix.checkerboard.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).mass i j = coarseMatrix.mass i j
          source
          theorem Verification.ApproximationExamples.shuffleMatrix_coarsen (i j : Fin 2) :
          (shuffleMatrix.checkMin.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).mass i j = (ProbabilityTheory.Copula.CellMass.product (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).mass i j
          source
          theorem Verification.ApproximationExamples.cellMass_ext {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} {A B : ProbabilityTheory.Copula.CellMass P Q} (h : ∀ (i : Fin m) (j : Fin n), A.mass i j = B.mass i j) :
          A = B
          source
          theorem Verification.ApproximationExamples.uniform_two_coord_zero (u : ↑unitInterval) :
          ↑((ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯).coord 0 u) = 2 * min (↑u) (1 / 2)
          source
          theorem Verification.ApproximationExamples.uniform_two_coord_one (u : ↑unitInterval) :
          ↑((ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯).coord 1 u) = 2 * ↑u - 2 * min (↑u) (1 / 2)
          source
          theorem Verification.ApproximationExamples.lowerMatrix_cdf (u v : ↑unitInterval) :
          lowerMatrix.checkerboard.cdf ![u, v] = ↑u * (↑((ProbabilityTheory.Copula.IntervalPartition.uniform 4 ⋯).coord 0 v) / 4 + ↑((ProbabilityTheory.Copula.IntervalPartition.uniform 4 ⋯).coord 2 v) / 2 + ↑((ProbabilityTheory.Copula.IntervalPartition.uniform 4 ⋯).coord 3 v) / 4) + min (↑u) (1 / 2) * (↑((ProbabilityTheory.Copula.IntervalPartition.uniform 4 ⋯).coord 1 v) - ↑((ProbabilityTheory.Copula.IntervalPartition.uniform 4 ⋯).coord 2 v)) / 2
          source
          theorem Verification.ApproximationExamples.lowerMatrix_si :
          lowerMatrix.checkerboard.IsSI
          source
          theorem Verification.ApproximationExamples.lower_counterexample :
          lowerMatrix.checkerboard.IsSI ∧ lowerMatrix.checkerboard.chatterjeeXi = 1 / 16 ∧ (lowerMatrix.checkerboard.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).checkerboard.chatterjeeXi = 1 / 8 ∧ lowerMatrix.checkerboard.chatterjeeXi < (lowerMatrix.checkerboard.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).checkerboard.chatterjeeXi

          Example 4.3, including the actual coarse cell masses and strict inequality.

          source
          theorem Verification.ApproximationExamples.upper_counterexample :
          upperMatrix.checkerboard.HasMTP2Density ∧ upperMatrix.checkerboard.chatterjeeXi = 5 / 8 ∧ (upperMatrix.checkerboard.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).checkMin.chatterjeeXi = 7 / 16 ∧ (upperMatrix.checkerboard.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).checkMin.chatterjeeXi < upperMatrix.checkerboard.chatterjeeXi

          Example 4.4, including a genuine MTP2 density and actual coarsening.

          source
          theorem Verification.ApproximationExamples.shuffle_counterexample :
          shuffleMatrix.checkMin.chatterjeeXi = 1 ∧ (shuffleMatrix.checkMin.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).checkMin.chatterjeeXi = 1 / 4

          The permutation example between Examples 4.3 and 4.4.