OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentrationCentered.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Exact centered coefficients for all covariant synthesis jets. The original frozen analyzing coefficient is split into its two monotone cutoffs and constant term, with no boundary-nullity premise.

  1. def OAI.LipschitzHilbert.SourceLatticePacket.physicalJetBand line 24
  2. def OAI.LipschitzHilbert.SourceLatticePacket.physicalJetVariation line 29
  3. def OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredJetBand line 33
  4. def OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredJetVariation line 38
  5. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalJetBand_continuous line 42
  6. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalJetVariation_continuous line 51
  7. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredJetBand_continuous line 62
  8. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredJetVariation_continuous line 71
  9. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalJetBand_eq_reference line 85
  10. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalJetVariation_normalization line 97
  11. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredJetBand_eq line 115
  12. theorem OAI.LipschitzHilbert.SourceLatticePacket.jetPartial_add_sub line 132
  13. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredJetPartial_eq line 142
  14. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredJetVariation_le line 160