OAI/Combinatorics/Progressions/Probability/AllocatedReferenceJetMass.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.BooleanCubeKernel.exists_physical_jet_density_mass line 15
  2. theorem OAI.Erdos3.BooleanCubeKernel.exists_physical_jet_singleton_window_mass line 85
  3. theorem OAI.Erdos3.BooleanCubeKernel.physicalWindow_sum_le_sampled_mass line 186
  4. theorem OAI.Erdos3.BooleanCubeKernel.physicalReconstruction_sum_le_sampled_mass line 220
  5. theorem OAI.Erdos3.BooleanCubeKernel.exists_reference_reconstruction_jet_mass line 278
  6. theorem OAI.Erdos3.BooleanCubeKernel.referenceJetEnvelope_volume line 382
  7. theorem OAI.Erdos3.BooleanCubeKernel.referenceJetEnvelope_anisotropic_volume line 402
  8. theorem OAI.Erdos3.BooleanCubeKernel.reference_density_spatial_error line 414
  9. def OAI.Erdos3.BooleanCubeKernel.coarseReferenceMassConstant line 471
  10. theorem OAI.Erdos3.BooleanCubeKernel.coarse_reference_density_spatial_error line 476
  11. theorem OAI.Erdos3.BooleanCubeKernel.coarse_reference_mean_spatial_budget line 504
  12. theorem OAI.Erdos3.BooleanCubeKernel.exists_coarse_reference_jet_mass line 550
  13. theorem OAI.Erdos3.BooleanCubeKernel.physicalReconstruction_normalized_mass_le line 622
  14. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_reference_jet_mass line 677