PlanarProfilePolarization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The common profile constants remain uniform under the four unit phases used in complex polarization. The proof uses their actual weighted Schwartz seminorm definition, without taking a maximum over the finite packet family.

theorem OAI.LipschitzHilbert.planarVerticalDerivative_add line 14
theorem OAI.LipschitzHilbert.planarHorizontalDerivative_add line 19
theorem OAI.LipschitzHilbert.planarVerticalJet_add line 25
theorem OAI.LipschitzHilbert.planarVerticalJet_smul line 29
theorem OAI.LipschitzHilbert.planarEnvelopeConstant_add_smul_le line 33
theorem OAI.LipschitzHilbert.planarProfileConstant_add_smul_le line 47
Source documentation
The precise common profile constant is subadditive under polarization, with the expected modulus of the scalar coefficient.
```
theorem planarProfileConstant_add_smul_le (f g : SchwartzMap (ℝ × ℝ) ℂ)
    (c : ℂ) (n : ℕ) :
    planarProfileConstant (f + c • g) n ≤
      planarProfileConstant f n + ‖c‖ * planarProfileConstant g n := by
…
```
Mentions: OAI.LipschitzHilbert.planarProfileConstant
theorem OAI.LipschitzHilbert.planarProfileConstant_add_unit_smul_le line 65

theorem OAI.LipschitzHilbert.planarProfileConstant_polarization_bound line 73

Source documentation

Two profiles with the same bound have polarization profiles bounded by twice that constant, uniformly for every unit complex phase.

theorem planarProfileConstant_polarization_bound (f g : SchwartzMap (ℝ × ℝ) ℂ)
    (c : ℂ) (hc : ‖c‖ = 1) (n : ℕ) (C : ℝ)
    (hf : planarProfileConstant f n ≤ C) (hg : planarProfileConstant g n ≤ C) :
    planarProfileConstant (f + c • g) n ≤ 2 * C := by
…

Mentions: OAI.LipschitzHilbert.planarProfileConstant