Norm.lean`

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ForestSpace.testValues line 19
Source documentation
All squared disjoint-segment tests. Quantifying over finite index types is equivalent to families S₁,...,Sₘ; a zero-sized family adds only zero to the set of test values.
Also declared: ComparatorChallenges/ForestSpace.lean:93 (same declaration text).
```
def testValues (u : V → ℝ) : Set ℝ :=
…
```
def OAI.ForestSpace.squareSup line 24
Also declared: ComparatorChallenges/ForestSpace.lean:98 (same declaration text).
def OAI.ForestSpace.rho line 28
Source documentation
Exactly the disjoint-segment norm, written as the square root of its squared testing supremum.
Also declared: ComparatorChallenges/ForestSpace.lean:102 (same declaration text).
```
noncomputable def rho (u : V → ℝ) : ℝ := Real.sqrt (squareSup u)
```
Mentions: OAI.ForestSpace.squareSup
theorem OAI.ForestSpace.zero_mem_testValues line 30
theorem OAI.ForestSpace.TestBound.bddAbove line 34
theorem OAI.ForestSpace.TestBound.squareSup_le line 40
theorem OAI.ForestSpace.testBound_squareSup line 46
theorem OAI.ForestSpace.squareSup_nonneg line 51
theorem OAI.ForestSpace.rho_nonneg line 54
theorem OAI.ForestSpace.rho_sq line 56
theorem OAI.ForestSpace.testBound_rho_sq line 59
theorem OAI.ForestSpace.rho_le_of_testBound line 63
theorem OAI.ForestSpace.testBound_of_rho_le line 67
theorem OAI.ForestSpace.rho_add_le line 71
theorem OAI.ForestSpace.rho_smul_le line 76
theorem OAI.ForestSpace.rho_zero line 82
theorem OAI.ForestSpace.rho_smul line 87
theorem OAI.ForestSpace.coordinate_le_rho line 100
def OAI.ForestSpace.l1size line 106
Distinct definitions of this name: ComparatorChallenges/ForestSpace.lean:104 (same statement text; different proof or body). Qualify references as OAI.ForestSpace.l1size@path.
theorem OAI.ForestSpace.l1size_nonneg line 109
theorem OAI.ForestSpace.finset_abs_sum_le_l1size line 113
theorem OAI.ForestSpace.testBound_l1size line 123
theorem OAI.ForestSpace.finsupp_has_testBound line 138
theorem OAI.ForestSpace.rho_le_l1size line 140
theorem OAI.ForestSpace.finsupp_rho_eq_zero line 143
theorem OAI.ForestSpace.nonempty_segment_iff_interval line 160
Source documentation
Nonempty finite convex chains are precisely the ancestral intervals. This rules out a change in the allowed segment tests.
```
theorem nonempty_segment_iff_interval (hF : ForestOrder V) (S : Finset V) :
    IsSegment S ∧ S.Nonempty ↔
      ∃ a b : V, a ≤ b ∧ ∀ v, v ∈ S ↔ a ≤ v ∧ v ≤ b := by
…
```
Mentions: OAI.ForestSpace.ForestOrder, OAI.ForestSpace.IsSegment
def OAI.ForestSpace.sourceNormValues line 178
Source documentation
The testing set with m≥1, nonempty segments, and the square root taken before the supremum.
```
def sourceNormValues (u : V → ℝ) : Set ℝ :=
…
```
theorem OAI.ForestSpace.sourceNormValues_nonempty line 184
theorem OAI.ForestSpace.sourceNormValues_le_rho line 193
theorem OAI.ForestSpace.sourceNormValues_bddAbove line 199
theorem OAI.ForestSpace.sourceNormValues_sup_nonneg line 203
theorem OAI.ForestSpace.testBound_from_source_sup line 213
Source documentation
Erasing empty zero tests and enumerating the remaining finite family does not alter its squared sum.
```
theorem testBound_from_source_sup [Nonempty V] {u : V → ℝ}
    (hu : ∃ C, TestBound u C) : TestBound u (sSup (sourceNormValues u)^2) := by
…
```
Mentions: OAI.ForestSpace.TestBound, OAI.ForestSpace.sourceNormValues
theorem OAI.ForestSpace.rho_eq_source_sup line 254
Source documentation
Equality with the nonempty-segment definition, including the exclusion of empty segments and zero-sized families and the order of supremum/square root.
```
theorem rho_eq_source_sup [Nonempty V] (u : V →₀ ℝ) :
    rho u = sSup (sourceNormValues u) := by
…
```
Mentions: OAI.ForestSpace.rho, OAI.ForestSpace.sourceNormValues