TileStructure.Forest.ψ_le_max

lemma ψ_le_max [ProofData a q K σ₁ σ₂ F G] {x : ℝ} : ψ x ≤ max 0 ((2 - 4 * x) ^ (a : ℝ)⁻¹) := by  by_cases! h₁ : x ≤ 1 / 4  · exact (ψ_le_one ..).trans ((Real.one_le_rpow (by linarith) (by simp)).trans (le_max_right ..))  by_cases! h₂ : 1 / 2 ≤ x  · rw [ψ_formula₄ h₂]; exact le_max_left ..  rw [ψ_formula₃ (one_lt_realD X) ⟨h₁.le, h₂.le⟩]  refine le_trans ?_ (le_max_right ..)  set y := 2 - 4 * x; apply Real.self_le_rpow_of_le_one  · unfold y; linarith  · unfold y; linarith  · exact Nat.cast_inv_le_one a