OAI/Analysis/LipschitzHilbert/Packets/PacketPolarization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact four-term polarization of a cross packet coefficient and synthesizing wave. Both packets may have different planar profiles.

  1. theorem OAI.LipschitzHilbert.packet_cross_polarization line 12
  2. theorem OAI.LipschitzHilbert.packet_cross_polarization_norm line 20