HistoryFourierConjugation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Conjugated leaves use the same Fourier profile at the signed frequency

theorem OAI.Ostmann.real_schwartz_fourier_conj line 13
theorem OAI.Ostmann.normalizedFourierProfile_conj line 25
theorem OAI.Ostmann.normalizedFourierProfile_fourier_conj line 35
Source documentation
The real physical smoothing function supplies the required symmetry; there is no additional analytic hypothesis on the Fourier profile.
```
theorem normalizedFourierProfile_fourier_conj (ψ : 𝓢(ℝ, ℂ))
    (hreal : ∀ x, conj (ψ x) = ψ x) (v z : ℝ) :
    conj (normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) v z) =
      normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) (-v) z :=
…
```
Mentions: OAI.Ostmann.normalizedFourierProfile

theorem OAI.Ostmann.signedFourierLeaves line 43

Source documentation

Arbitrarily conjugated bottom leaves are all represented by the existing unsigned formula family with their actual signed frequency parameters.

theorem signedFourierLeaves {n : ℕ} (ψ : 𝓢(ℝ, ℂ))
    (hreal : ∀ x, conj (ψ x) = ψ x) (v z : Fin n → ℝ) (sign : Fin n → Bool) :
    (∏ j, if sign j then normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) (v j) (z j)
      else conj (normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) (v j) (z j))) =
      ∏ j, normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) (if sign j then v j else -v j) (z j) := by
…

Mentions: OAI.Ostmann.normalizedFourierProfile