OAI/NumberTheory/DirichletL/Energy/SourceInputReindexGates.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.mass_map line 25
  2. lemma OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.nominal_map line 28
  3. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.ready_map line 33
  4. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.matches_map line 49
  5. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.matches_child line 58
  6. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.imageInput_matches line 69
  7. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.allocatedImage_matches line 79
  8. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.active_map line 93
  9. lemma OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.allocationLabels_map line 96
  10. lemma OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.actualAllocations_map line 103
  11. def OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.allocationEquiv line 111
  12. lemma OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.allocationEquiv_val line 124
  13. def OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.liveEquiv line 128
  14. lemma OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.liveEquiv_val line 140
  15. lemma OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.liveEquiv_symm_val line 143
  16. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.child_map line 146
  17. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.child_mass_map line 151
  18. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.child_volume_map line 157
  19. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.child_normalized_map line 163
  20. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.active_allocation_pullback line 169
  21. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.imageInput_ready line 177
  22. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.allocatedImage_ready line 183
  23. lemma OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.imageInput_mass line 190
  24. lemma OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.allocatedImage_mass line 194
  25. lemma OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.allocatedImage_volume line 200
  26. lemma OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.source_fields_map line 205
  27. theorem OAI.SevenEighths.CenteredMomentEnergySourceInputReindexGates.active_child_pullback line 215