LinearCost.lean`

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BoundedTreePotentials.linearCost line 18
Source documentation
Linear Hilbert-plus-path cost, with the Hilbert residual eliminated. This is exactly inf_{x=h+B μ} (‖h‖+‖μ‖), not the quadratic cost.
```
def linearCost (B : M →L[ℝ] H) (x : H) : ℝ :=
…
```
lemma OAI.BoundedTreePotentials.linearCost_bddBelow line 21
lemma OAI.BoundedTreePotentials.linearCost_nonneg line 25
lemma OAI.BoundedTreePotentials.linearCost_le line 28
lemma OAI.BoundedTreePotentials.linearCost_le_norm line 32
lemma OAI.BoundedTreePotentials.linearCost_zero line 36
lemma OAI.BoundedTreePotentials.linearCost_synthesis_le line 39
lemma OAI.BoundedTreePotentials.norm_le_mul_linearCost line 44
Source documentation
The lower comparison does not assume an attained decomposition.
```
lemma norm_le_mul_linearCost (B : M →L[ℝ] H) {K : ℝ} (hK : 1 ≤ K)
    (hB : ∀ μ : M, ‖B μ‖ ≤ K * ‖μ‖) (x : H) :
    ‖x‖ ≤ K * linearCost B x := by
…
```
Mentions: OAI.BoundedTreePotentials.linearCost
lemma OAI.BoundedTreePotentials.linearCost_add_le line 60
lemma OAI.BoundedTreePotentials.linearCost_smul_le line 75
def OAI.BoundedTreePotentials.linearCostSeminorm line 86
Source documentation
Seminorm supplied to Hahn--Banach in exact linear-cost duality.
```
def linearCostSeminorm (B : M →L[ℝ] H) : Seminorm ℝ H :=
…
```
lemma OAI.BoundedTreePotentials.exists_linear_norming line 92
Source documentation
Hahn--Banach for a seminorm, with the norming functional retained as an algebraic map so that the original Hilbert topology is not changed.
```
lemma exists_linear_norming {E : Type*} [AddCommGroup E] [Module ℝ E]
    (p : Seminorm ℝ E) (x : E) :
    ∃ φ : E →ₗ[ℝ] ℝ, φ x = p x ∧ ∀ z : E, |φ z| ≤ p z := by
…
```
lemma OAI.BoundedTreePotentials.linearCost_exists_norming line 106
lemma OAI.BoundedTreePotentials.inner_le_linearCost line 122
Source documentation
The easy direction of linear-cost duality, with absolute convergence abstracted into the bounded synthesis operator B.
```
lemma inner_le_linearCost (B : M →L[ℝ] H)
    {f : H} (hf : ‖f‖ ≤ 1) (hpath : ∀ μ : M, |inner ℝ f (B μ)| ≤ ‖μ‖)
    (x : H) : inner ℝ f x ≤ linearCost B x := by
…
```
Mentions: OAI.BoundedTreePotentials.linearCost
theorem OAI.BoundedTreePotentials.linearCost_exact_duality line 138
Source documentation
Exact infimal linear-cost duality. For root-path synthesis on ℓ₁(T_n), this gives the root-potential norming-set identity without assuming a minimizer.
```
theorem linearCost_exact_duality [CompleteSpace H]
    (B : M →L[ℝ] H) (x : H) :
    linearCost B x = sSup {r : ℝ | ∃ f : H, ‖f‖ ≤ 1 ∧
      (∀ μ : M, |inner ℝ f (B μ)| ≤ ‖μ‖) ∧ r = inner ℝ f x} := by
…
```
Mentions: OAI.BoundedTreePotentials.linearCost
abbrev OAI.BoundedTreePotentials.L1Mass line 167
lemma OAI.BoundedTreePotentials.l1_hasSum_norm line 169
lemma OAI.BoundedTreePotentials.atom_summable_norm line 172
lemma OAI.BoundedTreePotentials.atom_summable line 181
lemma OAI.BoundedTreePotentials.atom_tsum_norm_le line 185
def OAI.BoundedTreePotentials.atomSynthesis line 196
Source documentation
Absolutely convergent signed synthesis from ℓ₁.
```
def atomSynthesis (b : I → E) {K : ℝ} (hb : ∀ i, ‖b i‖ ≤ K) : L1Mass I →L[ℝ] E :=
…
```
Mentions: OAI.BoundedTreePotentials.L1Mass
lemma OAI.BoundedTreePotentials.atomSynthesis_apply line 207
lemma OAI.BoundedTreePotentials.atomSynthesis_single line 210
lemma OAI.BoundedTreePotentials.atom_pairing_bound line 222
lemma OAI.BoundedTreePotentials.atom_pairing_iff line 239
theorem OAI.BoundedTreePotentials.linearCost_atom_duality line 253
Source documentation
Exact duality with the individual atom constraints, rather than the equivalent but implicit constraint on arbitrary signed path mass.
```
theorem linearCost_atom_duality (b : I → E) {K : ℝ} (hb : ∀ i, ‖b i‖ ≤ K) (x : E) :
    linearCost (atomSynthesis b hb) x = sSup {r : ℝ | ∃ f : E, ‖f‖ ≤ 1 ∧
      (∀ i, |inner ℝ f (b i)| ≤ 1) ∧ r = inner ℝ f x} := by
…
```
Mentions: OAI.BoundedTreePotentials.linearCost, OAI.BoundedTreePotentials.atomSynthesis