Exponents

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Core.HeatPotential.heat_morrey_theta_zero_identity {γ θ₀ : ℝ} (hθ₀ : 1 / θ₀ = (2 - γ) / 5) : 2 - 5 / θ₀ = γ

theorem CKN.Core.HeatPotential.heat_morrey_theta_one_identity {γ θ₁ : ℝ} (hθ₁ : 1 / θ₁ = (1 - γ) / 5) : 1 - 5 / θ₁ = γ

theorem CKN.Core.HeatPotential.heat_morrey_geometric_ratio_lt_one {γ : ℝ} (hγ : γ < 1) : 2 ^ (γ - 1) < 1

theorem CKN.Core.HeatPotential.heat_morrey_geometric_ratio_nonneg {γ : ℝ} : 0 ≤ 2 ^ (γ - 1)

theorem CKN.Core.HeatPotential.heat_morrey_geometric_series {γ : ℝ} (hγ : γ < 1) : ∑' (j : ℕ), 2 ^ (↑j * (γ - 1)) = (1 - 2 ^ (γ - 1))⁻¹