AutoSamplingTheory.SALD.cycle114GeneralMovingTargetDiscreteCanonicalBarBStateEventSetIntegralDag

Data definition / provenance and workflow record

Meaning and type

The result has data type List AutoSamplingTheory.ProofDagBlock. A value of this type stores descriptions; it is not a proof of the statements in those descriptions.

def cycle114GeneralMovingTargetDiscreteCanonicalBarBStateEventSetIntegralDag :
    List ProofDagBlock

Construction and field-by-field explanation

Construct an ordered list of the following data items. It is not a logical conjunction or proof DAG.

This Lean definition constructs provenance or workflow data. It does not prove the mathematical statements stored as text. Status labels, named dependencies and citations are data, not compilation, proof or source certificates.

Ordered data items

1. id : String (explicit)

   Stable plan-node identifier.

   ASTIS.SALD.cycle114.lower_packet.canonical_barB_state_event_set_integral

   interface : String (explicit)

   Text describing intended mathematical interface.

   Compiled lower theorem: SALD.generalMovingTargetDiscreteCanonicalBarBStateSetIntegralOfCondDistrib proves hbarBStateSetIntegral for the canonical condDistrib representative on all source-facing state events {omega | hatXAtS omega in t}, using Mathlib's product conditional-expectation theorem and setIntegral_condExp.

   source : AutoSamplingTheory.SourceAnchor (explicit)

   Source pointer.

   AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteConditionalDriftSource — audited data reference, not expanded and not a compiled dependency edge

   targetLean : String (explicit)

   Textual planned implementation destination.

   AutoSamplingTheory/SALD.lean

   dependsOn : List String (explicit)

   Declared input names as strings, default empty.

   Ordered data items

   1. SALD.generalMovingTargetDiscreteCanonicalBarBStateSetIntegralOfCondDistrib
   2. ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib'
   3. MeasureTheory.setIntegral_condExp
   4. MeasureTheory.setIntegral_congr_ae
   5. appendix.tex:1368-1377

   reusedBy : List String (explicit)

   Declared consumers as strings, default empty.

   Ordered data items

   1. SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpStateFieldSetIntegralDef
   2. sald.general_moving_target_discrete.em_interpolation_fp
   3. sald.discrete_forward_kl.em_interpolation_fp
   4. thm:forward-KL-discrete

   status : AutoSamplingTheory.ProofStatus (explicit)

   Recorded workflow status, default planned.

   AutoSamplingTheory.ProofStatus.formalized — stored label only; no proof certification

2. id : String (explicit)

   Stable plan-node identifier.

   ASTIS.SALD.cycle114.remaining_named_barB_version_after_canonical_state_event_integral

   interface : String (explicit)

   Text describing intended mathematical interface.

   Remaining exact theorem after the canonical state-event narrowing: prove the paper-selected named barB is the canonical condDistrib representative hatRhoS-a.e., or instantiate the downstream EM route with the canonical representative; if a separate version is kept, also prove Integrable barB hatRhoS from the source construction.

   source : AutoSamplingTheory.SourceAnchor (explicit)

   Source pointer.

   AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteConditionalDriftSource — audited data reference, not expanded and not a compiled dependency edge

   targetLean : String (explicit)

   Textual planned implementation destination.

   AutoSamplingTheory/SALD.lean

   dependsOn : List String (explicit)

   Declared input names as strings, default empty.

   Ordered data items

   1. ASTIS.SALD.cycle113.remaining_named_barB_state_event_set_integral
   2. SALD.generalMovingTargetDiscreteCanonicalBarBStateSetIntegralOfCondDistrib
   3. SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpStateFieldSetIntegralDef
   4. appendix.tex:1368-1377

   reusedBy : List String (explicit)

   Declared consumers as strings, default empty.

   Ordered data items

   1. sald.general_moving_target_discrete.em_interpolation_fp
   2. sald.discrete_forward_kl.em_interpolation_fp
   3. thm:forward-KL-discrete

   status : AutoSamplingTheory.ProofStatus (explicit)

   Recorded workflow status, default planned.

   AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

def cycle114GeneralMovingTargetDiscreteCanonicalBarBStateEventSetIntegralDag :
    List ProofDagBlock :=
  [
    {
      id := "ASTIS.SALD.cycle114.lower_packet.canonical_barB_state_event_set_integral"
      interface := "Compiled lower theorem: SALD.generalMovingTargetDiscreteCanonicalBarBStateSetIntegralOfCondDistrib proves hbarBStateSetIntegral for the canonical condDistrib representative on all source-facing state events {omega | hatXAtS omega in t}, using Mathlib's product conditional-expectation theorem and setIntegral_condExp."
      source := saldGeneralMovingTargetDiscreteConditionalDriftSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "SALD.generalMovingTargetDiscreteCanonicalBarBStateSetIntegralOfCondDistrib",
        "ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib'",
        "MeasureTheory.setIntegral_condExp",
        "MeasureTheory.setIntegral_congr_ae",
        "appendix.tex:1368-1377"
      ]
      reusedBy := [
        "SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpStateFieldSetIntegralDef",
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp",
        "thm:forward-KL-discrete"
      ]
      status := ProofStatus.formalized
    },
    {
      id := "ASTIS.SALD.cycle114.remaining_named_barB_version_after_canonical_state_event_integral"
      interface := "Remaining exact theorem after the canonical state-event narrowing: prove the paper-selected named barB is the canonical condDistrib representative hatRhoS-a.e., or instantiate the downstream EM route with the canonical representative; if a separate version is kept, also prove Integrable barB hatRhoS from the source construction."
      source := saldGeneralMovingTargetDiscreteConditionalDriftSource
      targetLean := "AutoSamplingTheory/SALD.lean"
      dependsOn := [
        "ASTIS.SALD.cycle113.remaining_named_barB_state_event_set_integral",
        "SALD.generalMovingTargetDiscreteCanonicalBarBStateSetIntegralOfCondDistrib",
        "SALD.generalMovingTargetDiscreteCondDistribNamedBarBAeEqOfCondExpStateFieldSetIntegralDef",
        "appendix.tex:1368-1377"
      ]
      reusedBy := [
        "sald.general_moving_target_discrete.em_interpolation_fp",
        "sald.discrete_forward_kl.em_interpolation_fp",
        "thm:forward-KL-discrete"
      ]
      status := ProofStatus.obligation
    }
  ]

/-! ### Cycle 115: selected named `barB` version after canonical state events -/

/-- Cycle-115 middle obligation for the selected-version boundary left after
the canonical state-event set-integral theorem.

This packet stays on
`ASTIS.SALD.cycle114.remaining_named_barB_version_after_canonical_state_event_integral`
for `appendix.tex:1368-1377`.  It compiles the local theorem that turns the
smaller `hatRhoS`-a.e. selected-version equality into the old
`hbarBStateSetIntegral` input and into `Integrable barB hatRhoS`; it does not
prove the source selected-version equality itself.
-/