OAI/Analysis/LipschitzHilbert/Estimates/CoefficientPolarization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Antilinearity of the actual analyzing integral supplies the coefficients in the four-term packet polarization identity.

  1. theorem OAI.LipschitzHilbert.analyzingCoefficient_add_smul line 15