StartEnergy.lean`

47 declarations, 0 contain sorry, 0 declared as axioms

Segment start costs.

def OAI.BoundedTreePotentials.Segments.eTwo line 18
Source documentation
Extended Euclidean aggregation, with no finiteness assumption.
```
def eTwo {I : Type*} (f : I → ℝ≥0∞) : ℝ≥0∞ := (∑' i,f i^2)^(1/2:ℝ)
```
lemma OAI.BoundedTreePotentials.Segments.eTwo_sq line 20
lemma OAI.BoundedTreePotentials.Segments.eTwo_zero line 24
lemma OAI.BoundedTreePotentials.Segments.eTwo_mono line 26
lemma OAI.BoundedTreePotentials.Segments.eTwo_mul line 30
lemma OAI.BoundedTreePotentials.Segments.enn_sqrt_iSup line 37
lemma OAI.BoundedTreePotentials.Segments.enn_sq_iSup line 41
lemma OAI.BoundedTreePotentials.Segments.eTwo_eq_iSup line 46
lemma OAI.BoundedTreePotentials.Segments.eTwo_add line 50
lemma OAI.BoundedTreePotentials.Segments.eTwo_component line 61
lemma OAI.BoundedTreePotentials.Segments.enn_finset_sum_iSup line 66
lemma OAI.BoundedTreePotentials.Segments.enn_tsum_iSup line 76
lemma OAI.BoundedTreePotentials.Segments.eTwo_iSup line 84
lemma OAI.BoundedTreePotentials.Segments.startCost_mul line 91
lemma OAI.BoundedTreePotentials.Segments.startCost_add line 100
lemma OAI.BoundedTreePotentials.Segments.startCost_iSup line 118
lemma OAI.BoundedTreePotentials.Segments.enn_positive_energy_scalar line 133
lemma OAI.BoundedTreePotentials.Segments.startCost_positive_energy line 149
Source documentation
Positive energy holds even before restricting the recursion to finite costs.
```
lemma startCost_positive_energy (n : ℕ) (m r : List ℕ → ℝ≥0∞) :
    (startCost n m)^2+(startCost n r)^2 ≤ (startCost n (m+r))^2 := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.startCost
def OAI.BoundedTreePotentials.Segments.forestCost line 171
Source documentation
Nonnegative forest aggregation, with components indexed by root-inclusive heights n+1.
```
def forestCost (m : (n : ℕ) → List ℕ → ℝ≥0∞) : ℝ≥0∞ :=
…
```
lemma OAI.BoundedTreePotentials.Segments.forestCost_mono line 174
lemma OAI.BoundedTreePotentials.Segments.forestCost_add line 177
lemma OAI.BoundedTreePotentials.Segments.forestCost_mul line 180
lemma OAI.BoundedTreePotentials.Segments.forestCost_positive_energy line 184
lemma OAI.BoundedTreePotentials.Segments.forestCost_iSup line 190

lemma OAI.BoundedTreePotentials.Segments.enn_sum_iSup_le line 199

Source documentation

Independent choices may be made in each summand; no monotonicity of those choices is imposed.

lemma enn_sum_iSup_le {I : Type*} {J : I → Type*} [∀ i, Nonempty (J i)]
    (E : Finset I) (f : (i : I) → J i → ℝ≥0∞) {c : ℝ≥0∞}
    (h : ∀ a : (i : I) → J i, (∑ i ∈ E,f i (a i)) ≤ c) :
    (∑ i ∈ E,⨆ j,f i j) ≤ c := by
…

lemma OAI.BoundedTreePotentials.Segments.eTwo_inner_le line 222

def OAI.BoundedTreePotentials.Segments.treeSum line 235

Source documentation

Literal summation over all nodes up to height n.

def treeSum : ℕ → (List ℕ → ℝ≥0∞) → ℝ≥0∞
  | 0, m => m []
  | n+1, m => m []+∑' j : ℕ,treeSum n (fun s => m (j::s))

lemma OAI.BoundedTreePotentials.Segments.treeSum_zero line 239
lemma OAI.BoundedTreePotentials.Segments.treeSum_mono line 246
lemma OAI.BoundedTreePotentials.Segments.treeSum_tsum line 251
lemma OAI.BoundedTreePotentials.Segments.treeSum_mul line 261
lemma OAI.BoundedTreePotentials.Segments.treeSum_single line 270
lemma OAI.BoundedTreePotentials.Segments.treeSum_sq_le_startCost_sq line 300
Source documentation
Squaring and discarding nonnegative cross terms gives the exact lower Hilbert comparison before any tensor/quotient norm is introduced.
```
lemma treeSum_sq_le_startCost_sq (n : ℕ) (m : List ℕ → ℝ≥0∞) :
    treeSum n (fun s => (m s)^2) ≤ (startCost n m)^2 := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.treeSum, OAI.BoundedTreePotentials.Segments.startCost
def OAI.BoundedTreePotentials.Segments.IsPotential line 318
Source documentation
A nonnegative potential has Euclidean child values bounded by its parent.
```
def IsPotential : ℕ → (List ℕ → ℝ≥0∞) → Prop
  | 0, _ => True
  | n+1, b => eTwo (fun j : ℕ => b [j]) ≤ b [] ∧ ∀ j, IsPotential n (fun s => b (j::s))
```
Mentions: OAI.BoundedTreePotentials.Segments.eTwo
lemma OAI.BoundedTreePotentials.Segments.treeSum_pair_le line 322
lemma OAI.BoundedTreePotentials.Segments.startCost_congr line 338
lemma OAI.BoundedTreePotentials.Segments.treeSum_congr line 354
def OAI.BoundedTreePotentials.Segments.AntichainMass line 368
lemma OAI.BoundedTreePotentials.Segments.antichainMass_child line 371
lemma OAI.BoundedTreePotentials.Segments.startCost_antichain_sq line 380
Source documentation
Incomparable start masses combine in exact Euclidean norm. This is proved from the literal cost recursion, not used as a replacement definition.
```
lemma startCost_antichain_sq (n : ℕ) (m : List ℕ → ℝ≥0∞) (hm : AntichainMass n m) :
    (startCost n m)^2=treeSum n (fun s => (m s)^2) := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.AntichainMass, OAI.BoundedTreePotentials.Segments.startCost, OAI.BoundedTreePotentials.Segments.treeSum
lemma OAI.BoundedTreePotentials.Segments.forestCost_antichain_sq line 408
lemma OAI.BoundedTreePotentials.Segments.startCost_node_le line 416
lemma OAI.BoundedTreePotentials.Segments.forestCost_node_le line 430
lemma OAI.BoundedTreePotentials.Segments.forestCost_finset_sum line 434
lemma OAI.BoundedTreePotentials.Segments.forestCost_tsum line 448
Source documentation
Countable subadditivity follows from finite subadditivity and monotone continuity; the arrays need not have finite individual or total costs.
```
lemma forestCost_tsum {I : Type*} (m : I → (n : ℕ) → List ℕ → ℝ≥0∞) :
    forestCost (fun n s => ∑' i,m i n s) ≤ ∑' i,forestCost (m i) := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.forestCost
def OAI.BoundedTreePotentials.Segments.pathMass line 464
lemma OAI.BoundedTreePotentials.Segments.pathMass_le_startCost line 468