OAI/Combinatorics/EditApproximation/Refinement/PhysicalProgramLaw.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The global finite product of actual selection streams

Online slots and whole-cell slots form a finite disjoint union. Each slot contains its complete finite time array with the prescribed product law. Mapping the flattened product produces the actual online/group stream pair without independence hypotheses.

  1. abbrev OAI.EditApproximation.PhysicalOnlineKey line 26
  2. abbrev OAI.EditApproximation.PhysicalGroupKey line 29
  3. abbrev OAI.EditApproximation.PhysicalProgramKey line 34
  4. abbrev OAI.EditApproximation.PhysicalOnlineArray line 37
  5. abbrev OAI.EditApproximation.PhysicalGroupArray line 41
  6. abbrev OAI.EditApproximation.PhysicalProgramCoordinate line 46
  7. instance OAI.EditApproximation.physicalProgramCoordinateFintype line 51
  8. instance OAI.EditApproximation.physicalProgramCoordinateMeasurableSpace line 55
  9. instance OAI.EditApproximation.physicalProgramCoordinateMeasurableSingleton line 60
  10. abbrev OAI.EditApproximation.PhysicalProgramDraw line 66
  11. instance OAI.EditApproximation.physicalProgramBandMass_nezero line 69
  12. def OAI.EditApproximation.physicalProgramCoordinateLaw line 77
  13. instance OAI.EditApproximation.physicalProgramCoordinateLaw_probability line 92
  14. def OAI.EditApproximation.physicalProgramDrawLaw line 99
  15. instance OAI.EditApproximation.physicalProgramDrawLaw_probability line 103
  16. def OAI.EditApproximation.physicalProgramDrawStreams line 108
  17. def OAI.EditApproximation.physicalProgramStreamLaw line 115
  18. instance OAI.EditApproximation.physicalProgramStreamLaw_probability line 121
  19. theorem OAI.EditApproximation.physicalProgramStreamLaw_integral line 127

    Source documentation

    The transported law is the law of the complete literal stream pair.

    theorem physicalProgramStreamLaw_integral
    (payoff : PhysicalOnlineStreams source target U N P F A T thetaExponent H tau R ×
      PhysicalGroupStreams source target U N P F A thetaExponent Q R → ℝ) :
    (∫ streams, payoff streams ∂physicalProgramStreamLaw (R := R) source target U N P F A T thetaExponent H Q tau) =
…

    Mentions: OAI.EditApproximation.PhysicalOnlineStreams, OAI.EditApproximation.PhysicalGroupStreams, OAI.EditApproximation.physicalProgramStreamLaw

  20. def OAI.EditApproximation.physicalProgramRefresh line 138

    Source documentation

    Refresh exactly one online band and one shared whole-cell coordinate.

    noncomputable def physicalProgramRefresh
    (draw : PhysicalProgramDraw (R := R) source target U N P F A T thetaExponent H Q tau)
…

    Mentions: OAI.EditApproximation.PhysicalProgramDraw

  21. theorem OAI.EditApproximation.physicalProgramRefresh_online line 149
  22. theorem OAI.EditApproximation.physicalProgramRefresh_group line 165
  23. theorem OAI.EditApproximation.physicalProgramRefresh_online_other line 178
  24. theorem OAI.EditApproximation.physicalProgramRefresh_group_other line 198
  25. def OAI.EditApproximation.physicalProgramDrawSelections line 219

    Source documentation

    The actual complete selection program evaluated on its global array.

    def physicalProgramDrawSelections [NeZero R] (η κ : ℚ)
    (draw : PhysicalProgramDraw (R := R) source target U N P F A T thetaExponent H Q tau) :
…

    Mentions: OAI.EditApproximation.PhysicalProgramDraw

  26. theorem OAI.EditApproximation.physicalProgramDrawSelections_refresh_deeper line 228

    Source documentation

    Refreshing a parent's chosen band/cell coordinates leaves every strictly deeper raw selection function unchanged.

    theorem physicalProgramDrawSelections_refresh_deeper [NeZero R] (η κ : ℚ)
    (draw : PhysicalProgramDraw (R := R) source target U N P F A T thetaExponent H Q tau)
…

    Mentions: OAI.EditApproximation.PhysicalProgramDraw

  27. theorem OAI.EditApproximation.physicalProgramDrawLaw_refresh_integral line 264

    Source documentation

    Exact finite-product disintegration into an original global array and fresh local parent arrays. The unused old values are integrated out.

    theorem physicalProgramDrawLaw_refresh_integral
    (online : PhysicalOnlineKey source target U N P F A)
    (group : PhysicalGroupKey source target U N P F A thetaExponent)
    (payoff : PhysicalProgramDraw (R := R) source target U N P F A T thetaExponent H Q tau → ℝ) :
…

    Mentions: OAI.EditApproximation.PhysicalOnlineKey, OAI.EditApproximation.PhysicalGroupKey, OAI.EditApproximation.PhysicalProgramDraw