Coarse-graining support: Support.Book.Ch02.Theorems.ExistenceDefinitions

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

def HCPolySupport.Book.Ch02.ResponseMaximizerExists {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) : Prop

The existence statement needed to turn the note's v(.,U,p,q;a) into a chosen Lean object. This is a public theorem target, not a downstream hypothesis.

Equations

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

theorem HCPolySupport.Book.Ch02.ResponseMaximizerExists.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {p q : Vec d} (hv : ResponseMaximizerExists U a p q) : ResponseMaximizerExists U b p q

theorem HCPolySupport.Book.Ch02.ResponseMaximizerExists.iff_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {p q : Vec d} : ResponseMaximizerExists U a p q ↔ ResponseMaximizerExists U b p q

structure HCPolySupport.Book.Ch02.ResponseExistenceTheory {d : ℕ} (U : Domain d) (a : CoeffOn U) : Prop

Public theorem package for Chapter 2 response maximizer existence.

This contains only the existence package used by the chosen-object API. The proved public theorem is responseExistenceTheory in Existence.lean.

• exists_maximizer (p q : Vec d) : ResponseMaximizerExists U a p q

theorem HCPolySupport.Book.Ch02.ResponseExistenceTheory.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (hTheory : ResponseExistenceTheory U a) : ResponseExistenceTheory U b

theorem HCPolySupport.Book.Ch02.ResponseExistenceTheory.iff_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : ResponseExistenceTheory U a ↔ ResponseExistenceTheory U b

noncomputable def HCPolySupport.Book.Ch02.responseMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} (h : ResponseMaximizerExists U a p q) : Solution U a

Chosen public maximizer, once the Chapter 2 existence theorem has been supplied.

Equations

• HCPolySupport.Book.Ch02.responseMaximizer h = Classical.choose h

theorem HCPolySupport.Book.Ch02.responseMaximizer_meanZero {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} (h : ResponseMaximizerExists U a p q) : MeanZeroOn U.carrier (responseMaximizer h).toH1.toFun

theorem HCPolySupport.Book.Ch02.responseMaximizer_isMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} (h : ResponseMaximizerExists U a p q) : IsResponseMaximizer U a p q (responseMaximizer h)

theorem HCPolySupport.Book.Ch02.responseJ_eq_responseValue_responseMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} (h : ResponseMaximizerExists U a p q) : responseJ U a p q = responseValue U a p q (responseMaximizer h)

noncomputable def HCPolySupport.Book.Ch02.canonicalMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} (hTheory : ResponseExistenceTheory U a) (p q : Vec d) : CanonicalMaximizer U a p q

The canonical maximizer supplied by the public existence interface.

Equations

• HCPolySupport.Book.Ch02.canonicalMaximizer hTheory p q = { toSolution := HCPolySupport.Book.Ch02.responseMaximizer ⋯, meanZero := ⋯, isMaximizer := ⋯ }

theorem HCPolySupport.Book.Ch02.canonicalMaximizer_meanZero {d : ℕ} {U : Domain d} {a : CoeffOn U} (hTheory : ResponseExistenceTheory U a) (p q : Vec d) : MeanZeroOn U.carrier (canonicalMaximizer hTheory p q).toSolution.toH1.toFun

theorem HCPolySupport.Book.Ch02.canonicalMaximizer_isMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} (hTheory : ResponseExistenceTheory U a) (p q : Vec d) : IsResponseMaximizer U a p q (canonicalMaximizer hTheory p q).toSolution

theorem HCPolySupport.Book.Ch02.responseJ_eq_responseValue_canonicalMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} (hTheory : ResponseExistenceTheory U a) (p q : Vec d) : responseJ U a p q = responseValue U a p q (canonicalMaximizer hTheory p q).toSolution