OAI/Analysis/DiamondDistortion/SignCube.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DiamondDistortion.SignCube.History line 16
  2. instance OAI.DiamondDistortion.SignCube.(instance at line 19) line 19
  3. instance OAI.DiamondDistortion.SignCube.(instance at line 20) line 20
  4. lemma OAI.DiamondDistortion.SignCube.history_card line 21
  5. def OAI.DiamondDistortion.SignCube.mean line 27

    Source documentation

    Expectation for the uniform sign probability, written as iterated fair averages.

    def mean : (n : ℕ) → (History n → ℝ) → ℝ
  | 0,f => f ()
  | n+1,f => mean n (fun h => (f (h,false)+f (h,true))/2)

    Mentions: OAI.DiamondDistortion.SignCube.History

  6. lemma OAI.DiamondDistortion.SignCube.mean_zero line 30
  7. lemma OAI.DiamondDistortion.SignCube.mean_const line 32
  8. lemma OAI.DiamondDistortion.SignCube.mean_mono line 36
  9. lemma OAI.DiamondDistortion.SignCube.mean_nonneg line 40
  10. lemma OAI.DiamondDistortion.SignCube.mean_lower line 42
  11. lemma OAI.DiamondDistortion.SignCube.mean_upper line 44
  12. lemma OAI.DiamondDistortion.SignCube.mean_add line 46
  13. lemma OAI.DiamondDistortion.SignCube.mean_mul line 53
  14. lemma OAI.DiamondDistortion.SignCube.mean_sub line 60
  15. lemma OAI.DiamondDistortion.SignCube.mean_last line 65
  16. lemma OAI.DiamondDistortion.SignCube.mean_uniform line 67
  17. inductive OAI.DiamondDistortion.SignCube.Protocol line 77
  18. def OAI.DiamondDistortion.SignCube.Protocol.last line 83
  19. def OAI.DiamondDistortion.SignCube.Protocol.lastHead line 86
  20. def OAI.DiamondDistortion.SignCube.Protocol.Martingale line 92

    Source documentation

    Fair one-step conditional expectations. Iterating gives W_i=E(W_m|F_i).

    def Martingale : {n : ℕ} → Protocol X I n → Prop
  | 0,.initial _ _ => True
  | _+1,.extend T _ _ W => Martingale T ∧ ∀ h,T.last h=(1/2:ℝ) • (W (h,false)+W (h,true))
variable [Preorder I]

    Mentions: OAI.DiamondDistortion.SignCube.Protocol

  21. def OAI.DiamondDistortion.SignCube.Protocol.Nested line 96
  22. def OAI.DiamondDistortion.SignCube.Protocol.Anchored line 101

    Source documentation

    Each layer is between consecutive support heads, not separated by a new unrecorded head. This is imposed only for the inputs that require it.

    def Anchored : {n : ℕ} → Protocol X I n → Prop
  | 0,.initial _ _ => True
  | _+1,.extend T A _ _ => Anchored T ∧ ∀ h,A h=T.lastHead h
/-- Fixed across each level (stronger than predictability); required only by the
    deterministic leakage input. -/

    Mentions: OAI.DiamondDistortion.SignCube.Protocol

  23. def OAI.DiamondDistortion.SignCube.Protocol.CommonHeads line 106

    Source documentation

    Fixed across each level (stronger than predictability); required only by the deterministic leakage input.

    def CommonHeads : {n : ℕ} → Protocol X I n → Prop
  | 0,.initial _ _ => True
  | _+1,.extend T _ B _ => CommonHeads T ∧ ∃ H,∀ h,B h=H

    Mentions: OAI.DiamondDistortion.SignCube.Protocol

  24. def OAI.DiamondDistortion.SignCube.Protocol.Supported line 110
  25. def OAI.DiamondDistortion.SignCube.Protocol.childEnergy line 114
  26. def OAI.DiamondDistortion.SignCube.Protocol.parentEnergy line 116
  27. def OAI.DiamondDistortion.SignCube.Protocol.freshSum line 118
  28. def OAI.DiamondDistortion.SignCube.Protocol.leakageSum line 121
  29. def OAI.DiamondDistortion.SignCube.Protocol.terminalEnergy line 125
  30. lemma OAI.DiamondDistortion.SignCube.Protocol.terminalEnergy_nonneg line 126
  31. lemma OAI.DiamondDistortion.SignCube.Protocol.terminalEnergy_bound line 128
  32. lemma OAI.DiamondDistortion.SignCube.Protocol.freshSum_nonneg line 131
  33. lemma OAI.DiamondDistortion.SignCube.Protocol.leakageSum_nonneg line 135
  34. def OAI.DiamondDistortion.DirectLayers.SignInput line 146
  35. def OAI.DiamondDistortion.DirectLayers.PredictableInput line 150
  36. def OAI.DiamondDistortion.DirectLayers.LeakageInput line 154
  37. def OAI.DiamondDistortion.DirectLayers.GapInput line 157
  38. structure OAI.DiamondDistortion.DirectLayers.Regular line 161
  39. lemma OAI.DiamondDistortion.DirectLayers.Regular.finite_upper line 170
  40. lemma OAI.DiamondDistortion.DirectLayers.Regular.tail_norm line 182
  41. lemma OAI.DiamondDistortion.DirectLayers.Regular.capture line 186

    Source documentation

    A single larger ancestral head captures any finite family.

    lemma capture {κ : Type*} [Fintype κ] (H : I) (x : κ → X) {η : ℝ} (hη : 0 < η) :
    ∃ B : I,H ≤ B ∧ ∀ j,‖x j-A.projection B (x j)‖ < η := by
…
  42. lemma OAI.DiamondDistortion.DirectLayers.Regular.capture_one line 200
  43. lemma OAI.DiamondDistortion.DirectLayers.Regular.layer_parent line 204
  44. lemma OAI.DiamondDistortion.DirectLayers.select_tail line 211
  45. def OAI.DiamondDistortion.SignCube.Protocol.initialEnergy line 222
  46. lemma OAI.DiamondDistortion.SignCube.Protocol.initialEnergy_nonneg line 225
  47. lemma OAI.DiamondDistortion.SignCube.Protocol.common_last line 228
  48. lemma OAI.DiamondDistortion.SignCube.Protocol.supported_last line 233