OAI/Analysis/LipschitzHilbert/Trees/SourceNormalizedMotion.lean
2 declarations, 0 contain sorry, 0 declared as axioms
Mass normalization of the proved physical amplitude power gain. The local input is the raw physical motion, before multiplying by any mass power or hierarchy transition. No normalized motion is assumed.
- theorem
OAI.LipschitzHilbert.eventually_source_normalization_coefficientsline 19Source documentation
Both exact normalization coefficients have the smaller fixed power gain, uniformly over the source phase and block parameters.
theorem eventually_source_normalization_coefficients (D Q : ℝ) (hD : 0 ≤ D) (hQ : 0 ≤ Q) : ∀ᶠ L : ℝ in atTop, ∀ (Kw p μ : ℝ) (steps : ℕ) (Z : ℝ), 1 ≤ Kw → 1 ≤ p → 0 ≤ μ → μ ≤ 1 → (steps:ℝ) ≤ L^2 → 0 ≤ Z → Z ≤ 2*L^2 → let G := SourceParameters.step L … - theorem
OAI.LipschitzHilbert.eventually_source_normalized_motionline 85Source documentation
The source raw amplitude power gain, physical mass log motion and actual transition quotient estimate imply both normalized motion bounds. The raw bound is the conclusion of
source_physical_amplitude_power_gain.theorem eventually_source_normalized_motion (D Q : ℝ) (hD : 0 ≤ D) (hQ : 0 ≤ Q) : ∀ᶠ L : ℝ in atTop, ∀ (κ : Type) [Fintype κ], ∀ (Kw p μ n n' c c' : ℝ) (steps : ℕ) (Z : ℝ), 1 ≤ Kw → 1 ≤ p → 0 ≤ μ → μ ≤ 1 → 0 < n → 0 < n' → 0 < c → 0 < c' → (steps:ℝ) ≤ L^2 → 0 ≤ Z → Z ≤ 2*L^2 → ∀ (frequency : κ → ℝ) (b : ℝ) (A A' : EuclideanSpace ℂ κ) (lam lam' : ℂ), lam ≠ 0 → ‖lam‖ ≤ 1 → let G := SourceParameters.step L …