subDissipationDecayFactor

formal source

 137/-! ## Sub-dissipation Energy Decay -/
 138
 139/-- Energy decay ratio below the dissipation scale: φ⁻². -/
 140def subDissipationDecayFactor : ℝ := phi⁻¹ ^ 2
 141
 142/-- The decay factor is positive. -/
 143theorem subDissipationDecayFactor_pos : 0 < subDissipationDecayFactor :=
 144  pow_pos (inv_pos.mpr phi_pos) 2
 145
 146/-- The decay factor is strictly less than 1. -/
 147theorem subDissipationDecayFactor_lt_one : subDissipationDecayFactor < 1 := by
 148  unfold subDissipationDecayFactor
 149  have hlt : phi⁻¹ < 1 := inv_lt_one_of_one_lt₀ one_lt_phi
 150  nlinarith [sq_nonneg (1 - phi⁻¹), inv_pos.mpr phi_pos]
 151
 152/-- The sub-dissipation decay converges to zero: φ⁻²ⁿ → 0. -/
 153theorem sub_dissipation_decay_to_zero :
 154    Filter.Tendsto (fun k => subDissipationDecayFactor ^ k) Filter.atTop
 155    (nhds 0) :=
 156  tendsto_pow_atTop_nhds_zero_of_lt_one
 157    (le_of_lt subDissipationDecayFactor_pos)
 158    subDissipationDecayFactor_lt_one
 159
 160/-- After k ≥ 1 rungs below dissipation, energy is strictly less than 1. -/
 161theorem sub_dissipation_energy_decays {k : ℕ} (hk : 1 ≤ k) :
 162    subDissipationDecayFactor ^ k < 1 := by
 163  calc subDissipationDecayFactor ^ k
 164      ≤ subDissipationDecayFactor ^ 1 :=
 165        pow_le_pow_of_le_one (le_of_lt subDissipationDecayFactor_pos)
 166          (le_of_lt subDissipationDecayFactor_lt_one) hk
 167    _ = subDissipationDecayFactor := pow_one _
 168    _ < 1 := subDissipationDecayFactor_lt_one
 169
 170/-! ## The Wavenumber Ladder -/