SegmentNorm.lean`

128 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.DiamondDistortion.SegmentSystem line 13
Also declared: ComparatorChallenges/DiamondDistortion.lean:15 (same declaration text).
structure OAI.DiamondDistortion.SegmentSystem.Family line 21
Source documentation
The represented disjoint families in the definition of the primal segment norm.
Also declared: ComparatorChallenges/DiamondDistortion.lean:24 (same declaration text).
```
structure Family where
…
```
instance OAI.DiamondDistortion.SegmentSystem.(instance at line 27) line 27
def OAI.DiamondDistortion.SegmentSystem.Family.test line 36
Source documentation
Segment testing as a Euclidean-valued linear map.
Also declared: ComparatorChallenges/DiamondDistortion.lean:39 (same declaration text).
```
def Family.test (F : T.Family) : (ι →₀ ℝ) →ₗ[ℝ] EuclideanSpace ℝ (Fin F.n) where
…
```
theorem OAI.DiamondDistortion.SegmentSystem.Family.test_apply line 45
def OAI.DiamondDistortion.SegmentSystem.Family.seminorm line 48
Distinct definitions of this name: ComparatorChallenges/DiamondDistortion.lean:48 (same statement text; different proof or body). Qualify references as OAI.DiamondDistortion.SegmentSystem.Family.seminorm@path.
theorem OAI.DiamondDistortion.SegmentSystem.Family.seminorm_apply line 51
lemma OAI.DiamondDistortion.SegmentSystem.Family.test_single_le line 54
lemma OAI.DiamondDistortion.SegmentSystem.Family.test_le_l1 line 72
lemma OAI.DiamondDistortion.SegmentSystem.families_bddAbove line 86
def OAI.DiamondDistortion.SegmentSystem.primalSeminorm line 91
Also declared: ComparatorChallenges/DiamondDistortion.lean:53 (same declaration text).
lemma OAI.DiamondDistortion.SegmentSystem.test_le_primal line 93
lemma OAI.DiamondDistortion.SegmentSystem.primal_le_l1 line 100
def OAI.DiamondDistortion.SegmentSystem.singletonFamily line 108
Source documentation
Singleton families ensure that the segment seminorm separates points.
Also declared: ComparatorChallenges/DiamondDistortion.lean:56 (same declaration text).
```
def singletonFamily (v : ι) : T.Family where
…
```
lemma OAI.DiamondDistortion.SegmentSystem.coordinate_le_primal line 114
lemma OAI.DiamondDistortion.SegmentSystem.primal_eq_zero_iff line 120

def OAI.DiamondDistortion.SegmentSystem.familyOfFintype line 130

Source documentation

Finite families with any finite index type give the same segment tests.

def familyOfFintype {κ : Type*} [Fintype κ] (S : κ → Finset ι)
    (hS : ∀ i, T.IsSegment (S i))
    (hd : Pairwise (fun i j => Disjoint (S i) (S j))) : T.Family where
…

lemma OAI.DiamondDistortion.SegmentSystem.test_energy_le line 140

lemma OAI.DiamondDistortion.SegmentSystem.test_energy_le_allow_empty line 153

Source documentation

Empty pieces in a partition may be discarded; they contribute no energy.

lemma test_energy_le_allow_empty {κ : Type*} [Fintype κ] (S : κ → Finset ι)
    (hS : ∀ i, (S i).Nonempty → T.IsSegment (S i))
    (hd : Pairwise (fun i j => Disjoint (S i) (S j))) (u : ι →₀ ℝ) :
    (∑ i, (∑ v ∈ S i, u v) ^ 2) ≤ (T.primalSeminorm u) ^ 2 := by
…

def OAI.DiamondDistortion.SegmentSystem.Primal line 171
Also declared: ComparatorChallenges/DiamondDistortion.lean:62 (same declaration text).
def OAI.DiamondDistortion.SegmentSystem.ofPrimal line 174
Source documentation
Explicit conversions keep the chosen norm distinct from unrelated Finsupp structures.
```
def ofPrimal (u : T.Primal) : ι →₀ ℝ := u
```
def OAI.DiamondDistortion.SegmentSystem.toPrimal line 176
def OAI.DiamondDistortion.SegmentSystem.filterPrimal line 178
instance OAI.DiamondDistortion.SegmentSystem.(instance at line 181) line 181
instance OAI.DiamondDistortion.SegmentSystem.(instance at line 182) line 182
instance OAI.DiamondDistortion.SegmentSystem.(instance at line 185) line 185
instance OAI.DiamondDistortion.SegmentSystem.(instance at line 245) line 245
lemma OAI.DiamondDistortion.SegmentSystem.ofPrimal_sub line 248
lemma OAI.DiamondDistortion.SegmentSystem.ofPrimal_smul line 251
lemma OAI.DiamondDistortion.SegmentSystem.ofPrimal_sum line 254
lemma OAI.DiamondDistortion.SegmentSystem.ofPrimal_filter line 257
lemma OAI.DiamondDistortion.SegmentSystem.norm_eq_primal line 260
lemma OAI.DiamondDistortion.SegmentSystem.sub_filterPrimal line 263
abbrev OAI.DiamondDistortion.SegmentSystem.JamesSpace line 272
Also declared: ComparatorChallenges/DiamondDistortion.lean:130 (same declaration text).
abbrev OAI.DiamondDistortion.SegmentSystem.Dual line 275
Source documentation
Its full real continuous dual.
Also declared: ComparatorChallenges/DiamondDistortion.lean:133 (same declaration text).
```
abbrev Dual := StrongDual ℝ T.JamesSpace
```
def OAI.DiamondDistortion.SegmentSystem.coordinateFinite line 278
Source documentation
Coordinate evaluation on finite arrays, bounded by the singleton test.
Also declared: ComparatorChallenges/DiamondDistortion.lean:136 (same declaration text).
```
def coordinateFinite (v : ι) : T.Primal →L[ℝ] ℝ := by
…
```
def OAI.DiamondDistortion.SegmentSystem.coordinate line 331
Also declared: ComparatorChallenges/DiamondDistortion.lean:189 (same declaration text).
lemma OAI.DiamondDistortion.SegmentSystem.coordinate_coe line 334
def OAI.DiamondDistortion.SegmentSystem.unitFinite line 340
Source documentation
Primal unit coordinate and its canonical image in the completion.
Also declared: ComparatorChallenges/DiamondDistortion.lean:193 (same declaration text).
```
def unitFinite (v : ι) : T.Primal := Finsupp.single v 1
```
def OAI.DiamondDistortion.SegmentSystem.unitVector line 342
Also declared: ComparatorChallenges/DiamondDistortion.lean:195 (same declaration text).
lemma OAI.DiamondDistortion.SegmentSystem.norm_unitFinite line 344
lemma OAI.DiamondDistortion.SegmentSystem.norm_unitVector line 352
lemma OAI.DiamondDistortion.SegmentSystem.coordinate_unitVector line 355
def OAI.DiamondDistortion.SegmentSystem.headPrimal line 362
Source documentation
Finite head projection on the completed primal, defined even for nonancestral sets.
```
def headPrimal (H : Finset ι) : T.JamesSpace →L[ℝ] T.JamesSpace :=
…
```
lemma OAI.DiamondDistortion.SegmentSystem.headPrimal_apply line 365
lemma OAI.DiamondDistortion.SegmentSystem.sum_units_eq_filter line 369
lemma OAI.DiamondDistortion.SegmentSystem.headPrimal_coe line 383
def OAI.DiamondDistortion.SegmentSystem.headDual line 394
Also declared: ComparatorChallenges/DiamondDistortion.lean:197 (same declaration text).
lemma OAI.DiamondDistortion.SegmentSystem.headDual_apply line 397
lemma OAI.DiamondDistortion.SegmentSystem.headDual_apply_apply line 401
def OAI.DiamondDistortion.SegmentSystem.tailDual line 406
Source documentation
Complementary coordinate projection, never assumed contractive without proof.
```
def tailDual (H : Finset ι) : T.Dual →L[ℝ] T.Dual :=
…
```
lemma OAI.DiamondDistortion.SegmentSystem.tailDual_apply line 409
lemma OAI.DiamondDistortion.SegmentSystem.tailDual_apply_apply line 412
def OAI.DiamondDistortion.SegmentSystem.finiteEmbedding line 417
Source documentation
The canonical linear embedding, presented on actual finitely supported arrays.
```
def finiteEmbedding : (ι →₀ ℝ) →ₗ[ℝ] T.JamesSpace :=
…
```
lemma OAI.DiamondDistortion.SegmentSystem.finiteEmbedding_apply line 420
lemma OAI.DiamondDistortion.SegmentSystem.finiteEmbedding_single line 423
lemma OAI.DiamondDistortion.SegmentSystem.dual_coe_apply line 430
lemma OAI.DiamondDistortion.SegmentSystem.dual_ext line 440
Source documentation
Full dual functionals are determined by all coordinate unit vectors.
```
lemma dual_ext {x y : T.Dual} (h : ∀ v, x (T.unitVector v) = y (T.unitVector v)) : x = y := by
…
```
def OAI.DiamondDistortion.SegmentSystem.segmentFunctional line 447
lemma OAI.DiamondDistortion.SegmentSystem.segmentFunctional_coe line 449
lemma OAI.DiamondDistortion.SegmentSystem.segmentFunctional_unit line 453
def OAI.DiamondDistortion.SegmentSystem.combine line 459
Source documentation
Finite represented vectors retain their segment families as data.
```
def combine {κ : Type*} [Fintype κ] (S : κ → Finset ι) (a : κ → ℝ) : T.Dual :=
…
```
lemma OAI.DiamondDistortion.SegmentSystem.combine_coe line 462
lemma OAI.DiamondDistortion.SegmentSystem.combine_unit line 468
lemma OAI.DiamondDistortion.SegmentSystem.combine_add line 474
lemma OAI.DiamondDistortion.SegmentSystem.combine_sub line 478
lemma OAI.DiamondDistortion.SegmentSystem.combine_unit_of_mem line 486

lemma OAI.DiamondDistortion.SegmentSystem.norm_combine_le line 498

Source documentation

Cauchy--Schwarz for represented disjoint segment coefficients, with empty pieces permitted after a projection.

lemma norm_combine_le {κ : Type*} [Fintype κ] (S : κ → Finset ι) (a : κ → ℝ)
    (hS : ∀ i, (S i).Nonempty → T.IsSegment (S i))
    (hd : Pairwise (fun i j => Disjoint (S i) (S j))) :
    ‖T.combine S a‖ ≤ Real.sqrt (∑ i, (a i) ^ 2) := by
…

lemma OAI.DiamondDistortion.SegmentSystem.norm_cone_mean_le line 524

Source documentation

A finite family of disjoint cones can be tested by independently maximizing each cone's represented segment. This is the finite dual reconstruction bound.

lemma norm_cone_mean_le {Ω κ : Type*} [Fintype Ω] [Nonempty Ω] [Fintype κ]
    (S : Ω → κ → Finset ι) (a : Ω → κ → ℝ) (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω)
    (hS : ∀ ω g, (S ω g).Nonempty → T.IsSegment (S ω g))
    (hd : ∀ g h, g ≠ h → ∀ ω ν, Disjoint (S ω g) (S ν h)) :
    ‖∑ ω, w ω • T.combine (S ω) (a ω)‖ ≤
      Real.sqrt (∑ g, (∑ ω, w ω * |a ω g|) ^ 2) := by
…

lemma OAI.DiamondDistortion.SegmentSystem.combine_smul line 578
lemma OAI.DiamondDistortion.SegmentSystem.headDual_unit line 582
lemma OAI.DiamondDistortion.SegmentSystem.headDual_eq_self line 587
lemma OAI.DiamondDistortion.SegmentSystem.headDual_finite_apply line 596
lemma OAI.DiamondDistortion.SegmentSystem.headDual_commute line 604
lemma OAI.DiamondDistortion.SegmentSystem.tailDual_headDual line 611
def OAI.DiamondDistortion.SegmentSystem.headArray line 616
Source documentation
The array representing an arbitrary completed vector's finite head.
```
def headArray (H : Finset ι) (u : T.JamesSpace) : ι →₀ ℝ :=
…
```
lemma OAI.DiamondDistortion.SegmentSystem.headArray_outside line 619
lemma OAI.DiamondDistortion.SegmentSystem.finiteEmbedding_headArray line 625
lemma OAI.DiamondDistortion.SegmentSystem.headDual_segment line 630
lemma OAI.DiamondDistortion.SegmentSystem.tailDual_segment line 638
lemma OAI.DiamondDistortion.SegmentSystem.headDual_combine line 646
lemma OAI.DiamondDistortion.SegmentSystem.tailDual_combine line 650
abbrev OAI.DiamondDistortion.SegmentSystem.Coordinates line 654
def OAI.DiamondDistortion.SegmentSystem.coordinateTest line 656
lemma OAI.DiamondDistortion.SegmentSystem.coordinateTest_mem line 663
lemma OAI.DiamondDistortion.SegmentSystem.coordinateTest_not_mem line 666
lemma OAI.DiamondDistortion.SegmentSystem.coordinateTest_sum line 669
lemma OAI.DiamondDistortion.SegmentSystem.functional_pi_formula line 681
def OAI.DiamondDistortion.SegmentSystem.LocalFamily line 692
Source documentation
All local disjoint families. This type is finite even when the tree branches countably, because each member is a family of subsets of the fixed head K.
```
def LocalFamily (K : Finset ι) := {F : Finset (Finset ι) //
…
```
instance OAI.DiamondDistortion.SegmentSystem.localFamilyFintype line 695
abbrev OAI.DiamondDistortion.SegmentSystem.LocalIndex line 699
lemma OAI.DiamondDistortion.SegmentSystem.localFamily_subset line 701
lemma OAI.DiamondDistortion.SegmentSystem.localFamily_allowed line 705
lemma OAI.DiamondDistortion.SegmentSystem.localFamily_disjoint line 708
def OAI.DiamondDistortion.SegmentSystem.LocalFamily.asFamily line 715
def OAI.DiamondDistortion.SegmentSystem.LocalFamily.reindex line 724
lemma OAI.DiamondDistortion.SegmentSystem.LocalFamily.reindex_energy line 728
lemma OAI.DiamondDistortion.SegmentSystem.LocalFamily.reindex_combine line 735
lemma OAI.DiamondDistortion.SegmentSystem.LocalFamily.asFamily_subset line 742

def OAI.DiamondDistortion.SegmentSystem.localMap line 749

Source documentation

Local atoms as linear images of Euclidean blocks.

def localMap {K : Finset ι} (F : T.LocalFamily K) :
    EuclideanSpace ℝ (T.LocalIndex F) →ₗ[ℝ] T.Coordinates K where
…

lemma OAI.DiamondDistortion.SegmentSystem.localMap_combine line 767
lemma OAI.DiamondDistortion.SegmentSystem.functional_localMap line 772
lemma OAI.DiamondDistortion.SegmentSystem.finiteEmbedding_norm line 787
lemma OAI.DiamondDistortion.SegmentSystem.coordinateTest_pairing line 792
lemma OAI.DiamondDistortion.SegmentSystem.local_energy_le_of_functional_bound line 812
abbrev OAI.DiamondDistortion.SegmentSystem.Coefficients line 849
Source documentation
An l1-of-Euclidean-block ball gives a compact convex parameter space for all finite atomic combinations. No Caratheodory theorem is assumed.
```
abbrev Coefficients (K : Finset ι) :=
…
```
def OAI.DiamondDistortion.SegmentSystem.totalMap line 852
def OAI.DiamondDistortion.SegmentSystem.coefficientBall line 857
lemma OAI.DiamondDistortion.SegmentSystem.coefficientBall_compact line 860
lemma OAI.DiamondDistortion.SegmentSystem.coefficientBall_convex line 870
lemma OAI.DiamondDistortion.SegmentSystem.totalMap_single line 888
lemma OAI.DiamondDistortion.SegmentSystem.single_mem_coefficientBall line 898
structure OAI.DiamondDistortion.SegmentSystem.Atom line 910
Source documentation
A represented atom includes its coefficients, rather than just its value.
```
structure Atom (R : ℝ) where
…
```
def OAI.DiamondDistortion.SegmentSystem.Atom.value line 915
structure OAI.DiamondDistortion.SegmentSystem.AtomLaw line 919
Source documentation
Finite convex atom laws, with explicit probabilities and mean.
```
structure AtomLaw (Ω : Type*) [Fintype Ω] (R : ℝ) (x : T.Dual) where
…
```
def OAI.DiamondDistortion.SegmentSystem.zeroAtom line 926
lemma OAI.DiamondDistortion.SegmentSystem.zeroAtom_value line 935

def OAI.DiamondDistortion.SegmentSystem.blockAtom line 940

Source documentation

Normalize a local block to radius R. A zero block stays zero.

def blockAtom {K : Finset ι} (F : T.LocalFamily K)
    (a : EuclideanSpace ℝ (T.LocalIndex F)) {R : ℝ} (hR : 0 ≤ R) : T.Atom R where
…

lemma OAI.DiamondDistortion.SegmentSystem.blockAtom_value line 952
lemma OAI.DiamondDistortion.SegmentSystem.weighted_blockAtom line 958
lemma OAI.DiamondDistortion.SegmentSystem.representation_combine line 969

def OAI.DiamondDistortion.SegmentSystem.lawOfCoefficients line 991

Source documentation

Every block decomposition is a finite probability law, with its unused mass placed on the zero atom.

def lawOfCoefficients {K : Finset ι} (x : T.Dual) {R : ℝ} (hR : 0 < R)
    (c : T.Coefficients K) (hc : c ∈ T.coefficientBall K R)
    (hce : T.totalMap K c = fun v : K => x (T.unitVector v.val)) :
    T.AtomLaw (Option (T.LocalFamily K)) R (T.headDual K x) where
…

lemma OAI.DiamondDistortion.SegmentSystem.lawOfCoefficients_subset line 1019
structure OAI.DiamondDistortion.SegmentSystem.BipolarLaw line 1029
def OAI.DiamondDistortion.SegmentSystem.pairLaws line 1035
lemma OAI.DiamondDistortion.SegmentSystem.pairLaws_subset line 1069
def OAI.DiamondDistortion.SegmentSystem.CoordinatePredual line 1080
Source documentation
The norm-closed coordinate span, not the full infinite-tree dual.
Also declared: ComparatorChallenges/DiamondDistortion.lean:201 (same declaration text).
```
def CoordinatePredual : Submodule ℝ T.Dual :=
…
```
lemma OAI.DiamondDistortion.SegmentSystem.span_coordinates_finite_support line 1083