Named forms of the statements used (analytic case of r.LeBron.2)

LemmaUWith CU, LebronWith β C₀ μ C, WindowWith β C₀ c₁ Λ₁ are the bodies of LemmaUContract, LebronStepStatement, kappaSeq_window with the constants as parameters, so that helper lemmas can take them as hypotheses.

def AVenhance.Infra.FullTheorem.LemmaUWith (CU : ℝ) : Prop

Body of LemmaUContract with the constant a parameter.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.FullTheorem.lemmaU_with_of_contract (h : LemmaUContract) : ∃ (CU : ℝ), 0 < CU ∧ LemmaUWith CU

def AVenhance.Infra.FullTheorem.LebronWith (β C₀ μ C : ℝ) : Prop

Body of LebronStepStatement with the constants as parameters.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.FullTheorem.lebron_with_of_statement {β C₀ : ℝ} (h : LebronStepStatement β C₀) : ∃ (μ : ℝ) (C : ℝ), 0 < μ ∧ LebronWith β C₀ μ C

def AVenhance.Infra.FullTheorem.WindowWith (β C₀ c₁ Λ₁ : ℝ) : Prop

Body of kappaSeq_window with the constants as parameters.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.FullTheorem.window_with (β C₀ : ℝ) : ∃ (c₁ : ℝ) (Λ₁ : ℝ), 0 < c₁ ∧ WindowWith β C₀ c₁ Λ₁