OAI/Analysis/LipschitzHilbert/Trees/SourceLatticePolarization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Unit-phase profile combinations construct genuine source packet families on the same lattice with a factor-two change in the raw constant.

  1. theorem OAI.LipschitzHilbert.planarProfileJet_add_smul line 12
  2. theorem OAI.LipschitzHilbert.modulatedPlanarJet_add_smul line 19
  3. def OAI.LipschitzHilbert.SourceLatticePacket.withProfile line 37

    Source documentation

    Change the profiles, retaining every site, center, carrier and scale.

    def withProfile : SourceLatticePacket N κ ι :=
…

    Mentions: OAI.LipschitzHilbert.SourceLatticePacket

  4. def OAI.LipschitzHilbert.SourceLatticePacket.polarize line 41

    Source documentation

    A polarization family retains all geometry and twice the profile bound.

    def polarize (c : ℂ) (hc : ‖c‖ = 1) : SourceLatticePacket N κ ι :=
…

    Mentions: OAI.LipschitzHilbert.SourceLatticePacket

  5. theorem OAI.LipschitzHilbert.SourceLatticePacket.withProfile_length line 50
  6. theorem OAI.LipschitzHilbert.SourceLatticePacket.withProfile_actualX line 53
  7. theorem OAI.LipschitzHilbert.SourceLatticePacket.withProfile_actualZ line 56
  8. theorem OAI.LipschitzHilbert.SourceLatticePacket.withProfile_constant line 59
  9. theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_length line 61
  10. theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_actualX line 64
  11. theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_actualZ line 67
  12. theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_snappedSite line 70
  13. theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_raw line 74

    Source documentation

    Every raw covariant jet polarizes on the original geometry.

    theorem polarize_raw (c : ℂ) (hc : ‖c‖ = 1)
    (i : Fin 3) (j : Fin N) (u : ι j) (k : κ) (y : ℝ) :
    (P.polarize alt hAlt c hc).raw i j u k y =
      P.raw i j u k y + c • (P.withProfile alt hAlt).raw i j u k y := by
…

    Mentions: OAI.LipschitzHilbert.SourceLatticePacket.raw

  14. theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_constant line 85
  15. theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_family_wave line 90