OAI/Combinatorics/EditApproximation/Refinement/PhysicalSelectionResampling.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.physicalProgramResampleOnline line 23

   Source documentation

   Replacing exactly one parent's arrays leaves every other raw parent selection function unchanged. The replacement arrays retain their literal finite coordinate types.

   noncomputable def physicalProgramResampleOnline (stream : Online) (node : PhysicalInternalNode M J)
       (fresh : ∀ representative : Fin (stageRepresentatives source target U N P F A node.1).length,
         Fin R → Fin (optimizerTriangularMass
           (physicalProgramBandK source target U N P F A T thetaExponent H tau node representative))) : Online := by
   …

   Mentions: OAI.EditApproximation.PhysicalInternalNode, OAI.EditApproximation.stageRepresentatives, OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.physicalProgramBandK

2. def OAI.EditApproximation.physicalProgramResampleGroups line 30
3. theorem OAI.EditApproximation.physicalProgramResampleOnline_same line 40
4. theorem OAI.EditApproximation.physicalProgramResampleGroups_same line 45
5. theorem OAI.EditApproximation.physicalProgramResampleOnline_other line 50
6. theorem OAI.EditApproximation.physicalProgramResampleGroups_other line 56
7. theorem OAI.EditApproximation.physicalProgramSelections_online_congr_at line 64
8. theorem OAI.EditApproximation.physicalProgramSelections_groups_congr_at line 75
9. theorem OAI.EditApproximation.physicalProgramResample_deeper line 86
10. theorem OAI.EditApproximation.physicalProgram_online_action_mem line 111

    Source documentation

    Literal query-filtered selections contain the accepted physical sampler using the same complete child history.

    theorem physicalProgram_online_action_mem (online : Online) (groups : Groups) (delta : ℚ)
        (node : PhysicalInternalNode M J)
        (representative : Fin (stageRepresentatives source target U N P F A node.1).length) (b : ℕ)
        (member : UnskippedBand source target (physicalSourceInterval source.length node.1)
          b P thetaExponent tau F
          (physicalBandChildMassTable source target U N P F A T node.1 node.2)
          (physicalBandChildInitial source target U N P F A node.1 node.2))
        (hget : (stageRepresentatives source target U N P F A node.1).get representative = (b, member.center))
        (t : ℕ) (q : TargetInterval target.length)
        (hquery : physicalProgramOnlineGuard source target U N P F A node.1 q (b, member.center)) :
        sharedBandRationalAction member.center
          (physicalBandOnlineDraw source target U N P F A T delta (program online groups) node.1 node.2
    …

    Mentions: OAI.EditApproximation.PhysicalInternalNode, OAI.EditApproximation.stageRepresentatives, OAI.EditApproximation.UnskippedBand, OAI.EditApproximation.physicalSourceInterval, OAI.EditApproximation.physicalBandChildMassTable, OAI.EditApproximation.physicalBandChildInitial, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.physicalProgramOnlineGuard, OAI.EditApproximation.sharedBandRationalAction, OAI.EditApproximation.physicalBandOnlineDraw

11. theorem OAI.EditApproximation.physicalProgram_group_action_mem line 132