Dyadic stopping and logarithmic hull maxima

This file was automatically generated by Codex.

General finite dyadic path integration, restart packing, first-crossing cuts, and logarithmic caps on fixed-function hull maxima, together with complete finite trees, doubling-average segments and local maximal energy estimates. The retained estimates hold on whole cells, including points below removed cells. The grid and all statements are independent of the trilinear form and use only Mathlib and this module's definitions.

Source: blueprint/formalization_blueprint.tex, line 364, eq:path, path-packing, lem:cuts (lines 424–465), and lem:compression (lines 553–569). Verified library ingredients are finite sums and finite suprema, disjoint-union integration, Markov's inequality and the layer-cake formula.

structure TrilinearHT.Auto.RealDyadicGrid : Type

A real dyadic grid as in blueprint line 364. Each level is a translated interval partition; the alignment condition makes each coarse boundary a fine boundary.

• baseLength : ℝ

  Positive length of a cell at depth zero.

• baseLength_pos : 0 < self.baseLength
• origin : ℤ → ℝ

  Left endpoint of the coordinate origin at each depth.

• alignment (s : ℤ) : ∃ (k : ℤ), self.origin s = self.origin (s + 1) + ↑k * (self.baseLength * 2 ^ (-(s + 1)))

noncomputable def TrilinearHT.Auto.dyadicGridLength (G : RealDyadicGrid) (s : ℤ) : ℝ

Cell length at integer depth s in the grid G.

Equations

• TrilinearHT.Auto.dyadicGridLength G s = G.baseLength * 2 ^ (-s)

theorem TrilinearHT.Auto.dyadicGridLength_pos (G : RealDyadicGrid) (s : ℤ) : 0 < dyadicGridLength G s

noncomputable def TrilinearHT.Auto.dyadicGridLeft (G : RealDyadicGrid) (s m : ℤ) : ℝ

Left endpoint of the cell at depth s and integer position m.

Equations

• TrilinearHT.Auto.dyadicGridLeft G s m = G.origin s + ↑m * TrilinearHT.Auto.dyadicGridLength G s

noncomputable def TrilinearHT.Auto.dyadicGridCell (G : RealDyadicGrid) (s m : ℤ) : Set ℝ

Half-open cells, with integer depth and position, from blueprint line 364.

Equations

• TrilinearHT.Auto.dyadicGridCell G s m = Set.Ico (TrilinearHT.Auto.dyadicGridLeft G s m) (TrilinearHT.Auto.dyadicGridLeft G s m + TrilinearHT.Auto.dyadicGridLength G s)

theorem TrilinearHT.Auto.dyadicGridCell_measurable (G : RealDyadicGrid) (s m : ℤ) : MeasurableSet (dyadicGridCell G s m)

theorem TrilinearHT.Auto.dyadicGridCell_volume (G : RealDyadicGrid) (s m : ℤ) : MeasureTheory.volume (dyadicGridCell G s m) = ENNReal.ofReal (dyadicGridLength G s)

theorem TrilinearHT.Auto.dyadicGridCell_disjoint_of_lt (G : RealDyadicGrid) (s : ℤ) {m n : ℤ} (hmn : m < n) : Disjoint (dyadicGridCell G s m) (dyadicGridCell G s n)

theorem TrilinearHT.Auto.dyadicGridCell_pairwiseDisjoint (G : RealDyadicGrid) (s : ℤ) : Pairwise fun (m n : ℤ) => Disjoint (dyadicGridCell G s m) (dyadicGridCell G s n)

theorem TrilinearHT.Auto.dyadicGridCell_covers (G : RealDyadicGrid) (s : ℤ) (x : ℝ) : ∃ (m : ℤ), x ∈ dyadicGridCell G s m

theorem TrilinearHT.Auto.dyadicGridLength_half (G : RealDyadicGrid) (s : ℤ) : dyadicGridLength G (s + 1) * 2 = dyadicGridLength G s

theorem TrilinearHT.Auto.dyadicGridCell_children (G : RealDyadicGrid) (s m : ℤ) : ∃ (n : ℤ), dyadicGridCell G s m = dyadicGridCell G (s + 1) n ∪ dyadicGridCell G (s + 1) (n + 1)

Each source grid cell is exactly the union of its two consecutive children.

noncomputable def TrilinearHT.Auto.dyadicPathSum (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ENNReal) (x : ℝ) : ENNReal

The nonnegative path sum through a finite family of dyadic cells.

Equations

• TrilinearHT.Auto.dyadicPathSum G S a x = ∑ c ∈ S, (TrilinearHT.Auto.dyadicGridCell G c.1 c.2).indicator (fun (x : ℝ) => a c) x

theorem TrilinearHT.Auto.dyadicPathIntegral (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ENNReal) (R : Set ℝ) (hR : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ R) : ∑ c ∈ S, ENNReal.ofReal (dyadicGridLength G c.1) * a c = ∫⁻ (x : ℝ) in R, dyadicPathSum G S a x

Blueprint eq:path, lines 424–428: summing cell length times weight is exactly the integral of the path sum on a containing root.

theorem TrilinearHT.Auto.dyadicPathIntegral_real (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (R : Set ℝ) (hR : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ R) : ∑ c ∈ S, dyadicGridLength G c.1 * a c = ∫ (x : ℝ) in R, ∑ c ∈ S, (dyadicGridCell G c.1 c.2).indicator (fun (x : ℝ) => a c) x

The ordinary real-integral form of blueprint eq:path. It holds even for signed real weights, since the cell family is finite.

theorem TrilinearHT.Auto.finite_union_weight_le {ι : Type u_1} {α : Type u_2} [DecidableEq α] (T : Finset ι) (F : ι → Finset α) (w : α → ℝ) (hw : ∀ (x : α), 0 ≤ w x) : ∑ x ∈ T.biUnion F, w x ≤ ∑ i ∈ T, ∑ x ∈ F i, w x

theorem TrilinearHT.Auto.restart_generation_decay (g : ℕ → ℝ) {ρ L : ℝ} (hρ : 0 ≤ ρ) (hzero : g 0 ≤ L) (hstep : ∀ (k : ℕ), g (k + 1) ≤ ρ * g k) (k : ℕ) : g k ≤ ρ ^ k * L

Blueprint path-packing, line 429: every restart generation loses at least the fixed fraction 1 - ρ of total root length.

theorem TrilinearHT.Auto.restart_total_length (g : ℕ → ℝ) (hg : ∀ (k : ℕ), 0 ≤ g k) {ρ L : ℝ} (hρ : 0 ≤ ρ) (hρ1 : ρ < 1) (hzero : g 0 ≤ L) (hstep : ∀ (k : ℕ), g (k + 1) ≤ ρ * g k) : Summable g ∧ ∑' (k : ℕ), g k ≤ L / (1 - ρ)

Blueprint path-packing, line 429: the total length over all restart generations is summable and at most the initial root length divided by 1-ρ.

noncomputable def TrilinearHT.Auto.dyadicRootLength (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) : ℝ

Total length of a finite family of dyadic cells.

Equations

• TrilinearHT.Auto.dyadicRootLength G S = ∑ c ∈ S, TrilinearHT.Auto.dyadicGridLength G c.1

noncomputable def TrilinearHT.Auto.maximalDyadicCells (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) : Finset (ℤ × ℤ)

Maximal cells of a finite family, ordered by interval containment.

Equations

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

theorem TrilinearHT.Auto.maximalDyadicCells_subset (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) : maximalDyadicCells G S ⊆ S

theorem TrilinearHT.Auto.maximalDyadicCells_covers (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) {c : ℤ × ℤ} (hc : c ∈ S) : ∃ d ∈ maximalDyadicCells G S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2

theorem TrilinearHT.Auto.maximalDyadicCells_union (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) : ⋃ c ∈ maximalDyadicCells G S, dyadicGridCell G c.1 c.2 = ⋃ c ∈ S, dyadicGridCell G c.1 c.2

Passing to maximal cells preserves exactly the region removed by a finite stopping family.

theorem TrilinearHT.Auto.maximalDyadicCells_length_le (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) : dyadicRootLength G (maximalDyadicCells G S) ≤ dyadicRootLength G S

theorem TrilinearHT.Auto.dyadicGridCell_left_mem (G : RealDyadicGrid) (s m : ℤ) : dyadicGridLeft G s m ∈ dyadicGridCell G s m

theorem TrilinearHT.Auto.dyadicGridCell_sameDepth_common_point (G : RealDyadicGrid) (s m n : ℤ) {x : ℝ} (hm : x ∈ dyadicGridCell G s m) (hn : x ∈ dyadicGridCell G s n) : m = n

theorem TrilinearHT.Auto.dyadicGridCell_parent (G : RealDyadicGrid) (s n : ℤ) : ∃ (m : ℤ), dyadicGridCell G (s + 1) n ⊆ dyadicGridCell G s m

Every child cell belongs to a parent at the preceding depth.

theorem TrilinearHT.Auto.dyadicGridCell_ancestor (G : RealDyadicGrid) {s t : ℤ} (hst : s ≤ t) (n : ℤ) : ∃ (m : ℤ), dyadicGridCell G t n ⊆ dyadicGridCell G s m

theorem TrilinearHT.Auto.dyadicGridCell_nested_or_disjoint_of_le (G : RealDyadicGrid) {s t : ℤ} (hst : s ≤ t) (m n : ℤ) : Disjoint (dyadicGridCell G s m) (dyadicGridCell G t n) ∨ dyadicGridCell G t n ⊆ dyadicGridCell G s m

theorem TrilinearHT.Auto.dyadicGridCell_laminar (G : RealDyadicGrid) (c d : ℤ × ℤ) : Disjoint (dyadicGridCell G c.1 c.2) (dyadicGridCell G d.1 d.2) ∨ dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2 ∨ dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G c.1 c.2

Source dyadic cells are laminar: intersecting cells are nested.

theorem TrilinearHT.Auto.dyadicGridLength_strictAnti (G : RealDyadicGrid) : StrictAnti (dyadicGridLength G)

theorem TrilinearHT.Auto.dyadicGridCell_injective (G : RealDyadicGrid) : Function.Injective fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

theorem TrilinearHT.Auto.maximalDyadicCells_pairwiseDisjoint (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) : (↑(maximalDyadicCells G S)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

Distinct maximal cells are disjoint, the geometric fact used by the first-crossing cost estimate in lem:cuts.

noncomputable def TrilinearHT.Auto.dyadicAncestorSum (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (c : ℤ × ℤ) : ℝ

Sum of original data on ancestors, including the current cell.

Equations

• TrilinearHT.Auto.dyadicAncestorSum G S a c = ∑ d ∈ S with TrilinearHT.Auto.dyadicGridCell G c.1 c.2 ⊆ TrilinearHT.Auto.dyadicGridCell G d.1 d.2, a d

noncomputable def TrilinearHT.Auto.dyadicBadCells (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (T : ℝ) : Finset (ℤ × ℤ)

Cells whose cumulative ancestor weight exceeds the stopping threshold.

Equations

• TrilinearHT.Auto.dyadicBadCells G S a T = {c ∈ S | T < TrilinearHT.Auto.dyadicAncestorSum G S a c}

noncomputable def TrilinearHT.Auto.dyadicFirstCrossings (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (T : ℝ) : Finset (ℤ × ℤ)

First crossings are maximal violating cells; the violating value is excluded before its summand is included in the retained family.

Equations

• TrilinearHT.Auto.dyadicFirstCrossings G S a T = TrilinearHT.Auto.maximalDyadicCells G (TrilinearHT.Auto.dyadicBadCells G S a T)

noncomputable def TrilinearHT.Auto.dyadicRetainedCells (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (T : ℝ) : Finset (ℤ × ℤ)

Cells whose cumulative ancestor weight remains within the stopping threshold.

Equations

• TrilinearHT.Auto.dyadicRetainedCells G S a T = {c ∈ S | TrilinearHT.Auto.dyadicAncestorSum G S a c ≤ T}

theorem TrilinearHT.Auto.dyadicAncestorSum_mono (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ S, 0 ≤ a c) {c d : ℤ × ℤ} (hcd : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2) : dyadicAncestorSum G S a d ≤ dyadicAncestorSum G S a c

theorem TrilinearHT.Auto.dyadicFirstCrossings_mem (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (T : ℝ) {c : ℤ × ℤ} (hc : c ∈ dyadicFirstCrossings G S a T) : c ∈ S ∧ T < dyadicAncestorSum G S a c

theorem TrilinearHT.Auto.dyadicRetainedCells_iff (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ S, 0 ≤ a c) (T : ℝ) (c : ℤ × ℤ) : c ∈ dyadicRetainedCells G S a T ↔ c ∈ S ∧ ¬∃ d ∈ dyadicFirstCrossings G S a T, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2

Removing a first crossing removes exactly its cell and all original descendant summands. The data on earlier ancestors are left unchanged.

theorem TrilinearHT.Auto.dyadicFirstCrossings_pairwiseDisjoint (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (T : ℝ) : (↑(dyadicFirstCrossings G S a T)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

noncomputable def TrilinearHT.Auto.dyadicWeightedMass (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) : ℝ

Sum of cell lengths multiplied by their assigned weights.

Equations

• TrilinearHT.Auto.dyadicWeightedMass G S a = ∑ c ∈ S, TrilinearHT.Auto.dyadicGridLength G c.1 * a c

theorem TrilinearHT.Auto.dyadicWeightedMass_nonneg (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ S, 0 ≤ a c) : 0 ≤ dyadicWeightedMass G S a

theorem TrilinearHT.Auto.dyadicWeightedMass_ofReal (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ S, 0 ≤ a c) : ENNReal.ofReal (dyadicWeightedMass G S a) = ∑ c ∈ S, ENNReal.ofReal (dyadicGridLength G c.1) * ENNReal.ofReal (a c)

theorem TrilinearHT.Auto.dyadicAncestorSum_le_path (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ S, 0 ≤ a c) {c : ℤ × ℤ} {x : ℝ} (hx : x ∈ dyadicGridCell G c.1 c.2) : ENNReal.ofReal (dyadicAncestorSum G S a c) ≤ dyadicPathSum G S (fun (d : ℤ × ℤ) => ENNReal.ofReal (a d)) x

theorem TrilinearHT.Auto.dyadicFirstCrossings_weighted_cost (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ S, 0 ≤ a c) (R : Set ℝ) (hR : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ R) {T : ℝ} (hT : 0 ≤ T) : T * dyadicRootLength G (dyadicFirstCrossings G S a T) ≤ dyadicWeightedMass G S a

Integrating over the disjoint first crossings proves the Markov cost estimate before division by the positive crossing threshold.

theorem TrilinearHT.Auto.dyadicWeights_zero_of_mass_nonpos (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ S, 0 ≤ a c) (hW : dyadicWeightedMass G S a ≤ 0) (c : ℤ × ℤ) : c ∈ S → a c = 0

theorem TrilinearHT.Auto.dyadicAncestorSum_zero_of_mass_nonpos (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ S, 0 ≤ a c) (hW : dyadicWeightedMass G S a ≤ 0) (c : ℤ × ℤ) : dyadicAncestorSum G S a c = 0

theorem TrilinearHT.Auto.dyadicFirstCrossings_cost (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ S, 0 ≤ a c) (root : ℤ × ℤ) (hroot : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) {A ρ : ℝ} (hρ : 0 < ρ) (_hρ1 : ρ < 1) (hW : dyadicWeightedMass G S a ≤ A * dyadicGridLength G root.1) : dyadicRootLength G (dyadicFirstCrossings G S a (A / ρ)) ≤ ρ * dyadicGridLength G root.1

Blueprint lem:cuts, first assertion: first crossings of A/ρ cost at most ρ times the root length, including the zero-energy case.

noncomputable def TrilinearHT.Auto.dyadicRealPathSum (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (x : ℝ) : ℝ

Real-valued path sum of the original cell weights.

Equations

• TrilinearHT.Auto.dyadicRealPathSum G S a x = ∑ c ∈ S with x ∈ TrilinearHT.Auto.dyadicGridCell G c.1 c.2, a c

theorem TrilinearHT.Auto.dyadicRetainedPathSum_le (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ S, 0 ≤ a c) {T : ℝ} (hT : 0 ≤ T) (x : ℝ) : dyadicRealPathSum G (dyadicRetainedCells G S a T) a x ≤ T

Blueprint lem:cuts, first assertion: the retained path sum is bounded at every point, including points below a removed first-crossing cell.

theorem TrilinearHT.Auto.dyadicFirstCrossingCuts (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ S, 0 ≤ a c) (root : ℤ × ℤ) (hroot : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) {A ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ < 1) (hW : dyadicWeightedMass G S a ≤ A * dyadicGridLength G root.1) : dyadicRootLength G (dyadicFirstCrossings G S a (A / ρ)) ≤ ρ * dyadicGridLength G root.1 ∧ ∀ (x : ℝ), dyadicRealPathSum G (dyadicRetainedCells G S a (A / ρ)) a x ≤ A / ρ

Blueprint lem:cuts, complete first assertion with the specified first-crossing family and the everywhere retained bound.

noncomputable def TrilinearHT.Auto.dyadicEnergyAverage (G : RealDyadicGrid) (g : ℝ → ENNReal) (c : ℤ × ℤ) : ENNReal

Average of a nonnegative energy density on a dyadic cell.

Equations

• TrilinearHT.Auto.dyadicEnergyAverage G g c = (∫⁻ (x : ℝ) in TrilinearHT.Auto.dyadicGridCell G c.1 c.2, g x) / ENNReal.ofReal (TrilinearHT.Auto.dyadicGridLength G c.1)

noncomputable def TrilinearHT.Auto.dyadicHullMax (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (g : ℝ → ENNReal) (x : ℝ) : ENNReal

Full squared hull maximum, with value zero for an empty hull. The energy density is fixed, independently of any later stopping cells.

Equations

• TrilinearHT.Auto.dyadicHullMax G S g x = S.sup fun (c : ℤ × ℤ) => (TrilinearHT.Auto.dyadicGridCell G c.1 c.2).indicator (fun (x : ℝ) => TrilinearHT.Auto.dyadicEnergyAverage G g c) x

theorem TrilinearHT.Auto.dyadicHullMax_measurable (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (g : ℝ → ENNReal) : Measurable (dyadicHullMax G S g)

theorem TrilinearHT.Auto.dyadicHullMax_superlevel (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (g : ℝ → ENNReal) (t : ENNReal) : {x : ℝ | t < dyadicHullMax G S g x} = ⋃ c ∈ {c ∈ S | t < dyadicEnergyAverage G g c}, dyadicGridCell G c.1 c.2

A positive superlevel set is exactly the union of hull cells whose fixed energy averages exceed the level.

theorem TrilinearHT.Auto.dyadicHullMax_weak (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (g : ℝ → ENNReal) (R : Set ℝ) (hR : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ R) (t : ENNReal) : t * MeasureTheory.volume {x : ℝ | t < dyadicHullMax G S g x} ≤ ∫⁻ (x : ℝ) in R, g x

Blueprint lem:cuts, lines 453–457: the finite dyadic hull maximal operator has weak (1,1) constant one, even for extended-valued densities.

theorem TrilinearHT.Auto.dyadicHullMax_support_bound (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (g : ℝ → ENNReal) (t : ENNReal) : MeasureTheory.volume {x : ℝ | t < dyadicHullMax G S g x} ≤ MeasureTheory.volume (⋃ c ∈ maximalDyadicCells G S, dyadicGridCell G c.1 c.2)

The hull maximum vanishes outside the union of its maximal cells.

theorem TrilinearHT.Auto.bounded_layercake {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (f : α → ℝ) (hf : Measurable f) {T : ℝ} (hT : 0 ≤ T) (hf0 : ∀ (x : α), 0 ≤ f x) (hfT : ∀ (x : α), f x ≤ T) : ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ = ∫⁻ (t : ℝ) in Set.Ioc 0 T, μ {x : α | t < f x}

Layer cake for a bounded nonnegative real function, with the level integral restricted to its finite range.

theorem TrilinearHT.Auto.lintegral_ofReal_reciprocal {a T E : ℝ} (ha : 0 < a) (haT : a ≤ T) (hE : 0 ≤ E) : ∫⁻ (t : ℝ) in Set.Ioc a T, ENNReal.ofReal (E / t) = ENNReal.ofReal (E * Real.log (T / a))

The reciprocal tail in the weak (1,1) distribution integral gives the logarithm in blueprint lem:cuts, lines 458–462.

theorem TrilinearHT.Auto.weak_distribution_log_integral (F : ℝ → ENNReal) {E M T : ℝ} (hE : 0 < E) (hM : 0 < M) (hT : 0 ≤ T) (hsupport : ∀ (t : ℝ), 0 < t → F t ≤ ENNReal.ofReal M) (hweak : ∀ (t : ℝ), 0 < t → F t ≤ ENNReal.ofReal (E / t)) : ∫⁻ (t : ℝ) in Set.Ioc 0 T, F t ≤ ENNReal.ofReal (E * (1 + Real.log (2 + M * T / E)))

Integrating a distribution bounded by min(M,E/t) up to T gives the logarithmic truncation bound used in lem:cuts.

theorem TrilinearHT.Auto.weak_distribution_log_integral_nonneg (F : ℝ → ENNReal) {E M T : ℝ} (hE : 0 ≤ E) (hM : 0 ≤ M) (hT : 0 ≤ T) (hsupport : ∀ (t : ℝ), 0 < t → F t ≤ ENNReal.ofReal M) (hweak : ∀ (t : ℝ), 0 < t → F t ≤ ENNReal.ofReal (E / t)) : ∫⁻ (t : ℝ) in Set.Ioc 0 T, F t ≤ ENNReal.ofReal (E * (1 + Real.log (2 + M * T / E)))

theorem TrilinearHT.Auto.finite_family_log_integral {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (V : Finset ι) (f : ι → α → ℝ) (hf : ∀ ν ∈ V, Measurable (f ν)) {E M T : ℝ} (hE : 0 ≤ E) (hM : 0 ≤ M) (hT : 0 ≤ T) (hf0 : ∀ ν ∈ V, ∀ (x : α), 0 ≤ f ν x) (hfT : ∀ ν ∈ V, ∀ (x : α), f ν x ≤ T) (hsupport : ∀ (t : ℝ), 0 < t → ∑ ν ∈ V, μ {x : α | t < f ν x} ≤ ENNReal.ofReal M) (hweak : ∀ (t : ℝ), 0 < t → ∑ ν ∈ V, μ {x : α | t < f ν x} ≤ ENNReal.ofReal (E / t)) : ∑ ν ∈ V, ∫⁻ (x : α), ENNReal.ofReal (f ν x) ∂μ ≤ ENNReal.ofReal (E * (1 + Real.log (2 + M * T / E)))

Finite-family layer cake and the weak/support distribution bounds yield a logarithmic integral estimate, including zero energy and zero support.

theorem TrilinearHT.Auto.truncated_family_log_integral {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (V : Finset ι) (m : ι → α → ENNReal) (hm : ∀ ν ∈ V, Measurable (m ν)) {E M T : ℝ} (hE : 0 ≤ E) (hM : 0 ≤ M) (hT : 0 ≤ T) (hdist : ∀ (t : ℝ), 0 < t → ∑ ν ∈ V, μ {x : α | ENNReal.ofReal t < m ν x} ≤ min (ENNReal.ofReal M) (ENNReal.ofReal (E / t))) : ∑ ν ∈ V, ∫⁻ (x : α), min (m ν x) (ENNReal.ofReal T) ∂μ ≤ ENNReal.ofReal (E * (1 + Real.log (2 + M * T / E)))

Logarithmic integral estimate for a finite family of truncated extended-valued maxima from their summed distribution bound.

theorem TrilinearHT.Auto.dyadicHullMax_log_integral {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (R : Set ℝ) (hR : ∀ ν ∈ V, ∀ c ∈ S ν, dyadicGridCell G c.1 c.2 ⊆ R) {E M T : ℝ} (hE0 : 0 ≤ E) (hM0 : 0 ≤ M) (hT : 0 ≤ T) (hE : ∑ ν ∈ V, ∫⁻ (x : ℝ) in R, g ν x ≤ ENNReal.ofReal E) (hM : ∑ ν ∈ V, MeasureTheory.volume (⋃ c ∈ maximalDyadicCells G (S ν), dyadicGridCell G c.1 c.2) ≤ ENNReal.ofReal M) : ∑ ν ∈ V, ∫⁻ (x : ℝ), min (dyadicHullMax G (S ν) (g ν) x) (ENNReal.ofReal T) ≤ ENNReal.ofReal (E * (1 + Real.log (2 + M * T / E)))

Blueprint lem:cuts, lines 458–462: the sum of the integrals of truncated fixed hull maxima is bounded logarithmically by total energy and total hull support. This unnormalized form includes zero energy.

noncomputable def TrilinearHT.Auto.dyadicPartialHullMax (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (g : ℝ → ENNReal) (c : ℤ × ℤ) : ENNReal

Partial squared hull maximum using only ancestors through the current cell. All energy averages still use the original fixed function.

Equations

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

theorem TrilinearHT.Auto.dyadicPartialHullMax_mono (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (g : ℝ → ENNReal) {c d : ℤ × ℤ} (hcd : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2) : dyadicPartialHullMax G H g d ≤ dyadicPartialHullMax G H g c

theorem TrilinearHT.Auto.dyadicPartialHullMax_le_full (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (g : ℝ → ENNReal) {c : ℤ × ℤ} {x : ℝ} (hx : x ∈ dyadicGridCell G c.1 c.2) : dyadicPartialHullMax G H g c ≤ dyadicHullMax G H g x

theorem TrilinearHT.Auto.dyadicEnergyAverage_le_partial (G : RealDyadicGrid) (H : Finset (ℤ × ℤ)) (g : ℝ → ENNReal) {c : ℤ × ℤ} (hc : c ∈ H) : dyadicEnergyAverage G g c ≤ dyadicPartialHullMax G H g c

theorem TrilinearHT.Auto.dyadicPartialHullMax_sum_eq_truncated {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (c : ℤ × ℤ) {T : ENNReal} (hT : ∀ ν ∈ V, dyadicPartialHullMax G (H ν) (g ν) c ≤ T) : ∑ ν ∈ V, dyadicPartialHullMax G (H ν) (g ν) c = ∑ ν ∈ V, min (dyadicPartialHullMax G (H ν) (g ν) c) T

Before any individual threshold is crossed, the partial sum agrees with its truncated version, as required by lem:cuts, line 463.

def TrilinearHT.Auto.dyadicHullGood {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (T U : ENNReal) (c : ℤ × ℤ) : Prop

A cell is good for both rules if no partial individual maximum exceeds T and the sum of truncated partial maxima does not exceed U.

Equations

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

noncomputable def TrilinearHT.Auto.dyadicHullCuts {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (T U : ENNReal) : Finset (ℤ × ℤ)

The combined first crossings, chosen as maximal cells violating at least one of the two partial-max rules.

Equations

• TrilinearHT.Auto.dyadicHullCuts V G S H g T U = TrilinearHT.Auto.maximalDyadicCells G ({c ∈ S | ¬TrilinearHT.Auto.dyadicHullGood V G H g T U c})

theorem TrilinearHT.Auto.dyadicHullGood_ancestor {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (T U : ENNReal) {c d : ℤ × ℤ} (hcd : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2) (hc : dyadicHullGood V G H g T U c) : dyadicHullGood V G H g T U d

theorem TrilinearHT.Auto.dyadicRootLength_ofReal_eq_volume (G : RealDyadicGrid) (C : Finset (ℤ × ℤ)) (hC : (↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2) : ENNReal.ofReal (dyadicRootLength G C) = MeasureTheory.volume (⋃ c ∈ C, dyadicGridCell G c.1 c.2)

theorem TrilinearHT.Auto.dyadicHullCuts_cover_bad {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (T U : ENNReal) : ⋃ c ∈ dyadicHullCuts V G S H g T U, dyadicGridCell G c.1 c.2 ⊆ (⋃ ν ∈ V, {x : ℝ | T < dyadicHullMax G (H ν) (g ν) x}) ∪ {x : ℝ | U < ∑ ν ∈ V, min (dyadicHullMax G (H ν) (g ν) x) T}

Each removed cell lies on its entirety in the union of the full individual superlevel sets or the full truncated-sum superlevel set.

theorem TrilinearHT.Auto.dyadicHullCuts_cost {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (R : Set ℝ) (hR : ∀ ν ∈ V, ∀ c ∈ H ν, dyadicGridCell G c.1 c.2 ⊆ R) {E M T U : ℝ} (hE0 : 0 ≤ E) (hM0 : 0 ≤ M) (hT : 0 < T) (hU : 0 < U) (hE : ∑ ν ∈ V, ∫⁻ (x : ℝ) in R, g ν x ≤ ENNReal.ofReal E) (hM : ∑ ν ∈ V, MeasureTheory.volume (⋃ c ∈ maximalDyadicCells G (H ν), dyadicGridCell G c.1 c.2) ≤ ENNReal.ofReal M) : dyadicRootLength G (dyadicHullCuts V G S H g (ENNReal.ofReal T) (ENNReal.ofReal U)) ≤ E / T + E * (1 + Real.log (2 + M * T / E)) / U

The combined first-crossing length is bounded by the individual weak cost plus the truncated-sum Markov cost. This proves both stopping rules in blueprint lem:cuts, lines 458 and 463–465, before choosing thresholds.

theorem TrilinearHT.Auto.dyadicHullCuts_cost_normalized {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (root : ℤ × ℤ) (hR : ∀ ν ∈ V, ∀ c ∈ H ν, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) {E M T U : ℝ} (hE0 : 0 ≤ E) (hM0 : 0 ≤ M) (hT : 0 < T) (hU : 0 < U) (hE : ∑ ν ∈ V, ∫⁻ (x : ℝ) in dyadicGridCell G root.1 root.2, g ν x ≤ ENNReal.ofReal (E * dyadicGridLength G root.1)) (hM : ∑ ν ∈ V, MeasureTheory.volume (⋃ c ∈ maximalDyadicCells G (H ν), dyadicGridCell G c.1 c.2) ≤ ENNReal.ofReal (M * dyadicGridLength G root.1)) : dyadicRootLength G (dyadicHullCuts V G S H g (ENNReal.ofReal T) (ENNReal.ofReal U)) ≤ (E / T + E * (1 + Real.log (2 + M * T / E)) / U) * dyadicGridLength G root.1

theorem TrilinearHT.Auto.dyadicHullCuts_cost_selected_pos {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (root : ℤ × ℤ) (hR : ∀ ν ∈ V, ∀ c ∈ H ν, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) {E M ρ : ℝ} (hE0 : 0 < E) (hM0 : 0 ≤ M) (hρ : 0 < ρ) (hE : ∑ ν ∈ V, ∫⁻ (x : ℝ) in dyadicGridCell G root.1 root.2, g ν x ≤ ENNReal.ofReal (E * dyadicGridLength G root.1)) (hM : ∑ ν ∈ V, MeasureTheory.volume (⋃ c ∈ maximalDyadicCells G (H ν), dyadicGridCell G c.1 c.2) ≤ ENNReal.ofReal (M * dyadicGridLength G root.1)) : dyadicRootLength G (dyadicHullCuts V G S H g (ENNReal.ofReal (2 * E / ρ)) (ENNReal.ofReal (2 * E / ρ * (1 + Real.log (2 + 2 * M / ρ))))) ≤ ρ * dyadicGridLength G root.1

Explicit threshold choices allocate half the cut budget to each rule in the positive-energy case of lem:cuts.

theorem TrilinearHT.Auto.dyadicPartialHullMax_zero_of_energy {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (R : Set ℝ) (hR : ∀ ν ∈ V, ∀ c ∈ H ν, dyadicGridCell G c.1 c.2 ⊆ R) (hE : ∑ ν ∈ V, ∫⁻ (x : ℝ) in R, g ν x ≤ 0) (ν : ι) (hν : ν ∈ V) (c : ℤ × ℤ) : dyadicPartialHullMax G (H ν) (g ν) c = 0

theorem TrilinearHT.Auto.dyadicHullCuts_empty_of_energy_zero {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (R : Set ℝ) (hR : ∀ ν ∈ V, ∀ c ∈ H ν, dyadicGridCell G c.1 c.2 ⊆ R) (hE : ∑ ν ∈ V, ∫⁻ (x : ℝ) in R, g ν x ≤ 0) (T U : ENNReal) : dyadicHullCuts V G S H g T U = ∅

theorem TrilinearHT.Auto.dyadicHullCuts_cost_selected {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (root : ℤ × ℤ) (hR : ∀ ν ∈ V, ∀ c ∈ H ν, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) {E M ρ : ℝ} (hE0 : 0 ≤ E) (hM0 : 0 ≤ M) (hρ : 0 < ρ) (hE : ∑ ν ∈ V, ∫⁻ (x : ℝ) in dyadicGridCell G root.1 root.2, g ν x ≤ ENNReal.ofReal (E * dyadicGridLength G root.1)) (hM : ∑ ν ∈ V, MeasureTheory.volume (⋃ c ∈ maximalDyadicCells G (H ν), dyadicGridCell G c.1 c.2) ≤ ENNReal.ofReal (M * dyadicGridLength G root.1)) : dyadicRootLength G (dyadicHullCuts V G S H g (ENNReal.ofReal (2 * E / ρ)) (ENNReal.ofReal (2 * E / ρ * (1 + Real.log (2 + 2 * M / ρ))))) ≤ ρ * dyadicGridLength G root.1

Blueprint lem:cuts: the selected combined first crossings cost at most ρ times the root length, including the zero-energy case.

noncomputable def TrilinearHT.Auto.dyadicHullRetained {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (T U : ENNReal) : Finset (ℤ × ℤ)

Retained cells satisfy both partial-max rules; their equivalence with deleting whole first-crossing subtrees is proved below.

Equations

• TrilinearHT.Auto.dyadicHullRetained V G S H g T U = Finset.filter (TrilinearHT.Auto.dyadicHullGood V G H g T U) S

theorem TrilinearHT.Auto.dyadicHullRetained_iff {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (T U : ENNReal) (c : ℤ × ℤ) : c ∈ dyadicHullRetained V G S H g T U ↔ c ∈ S ∧ ¬∃ d ∈ dyadicHullCuts V G S H g T U, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2

theorem TrilinearHT.Auto.dyadicHullRetained_cap {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (hHS : ∀ ν ∈ V, H ν ⊆ S) (T U : ENNReal) (x : ℝ) : ∑ ν ∈ V, dyadicHullMax G (dyadicHullRetained V G (H ν) H g T U) (g ν) x ≤ U

Blueprint eq:hull-cap: the fixed-function maxima on whole retained hull cells satisfy the sum threshold at every point, even below a cut.

noncomputable def TrilinearHT.Auto.hullCutConstant (ρ : ℝ) : ℝ

An explicit source-admissible constant depending only on the cut fraction, for the hull cap in lem:cuts.

Equations

• TrilinearHT.Auto.hullCutConstant ρ = 2 / ρ * (1 + Real.log (2 / ρ))

theorem TrilinearHT.Auto.hullCutConstant_pos {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ < 1) : 0 < hullCutConstant ρ

theorem TrilinearHT.Auto.hullCutThreshold_le {E M ρ : ℝ} (hE : 0 ≤ E) (hM : 0 ≤ M) (hρ : 0 < ρ) (hρ1 : ρ < 1) : 2 * E / ρ * (1 + Real.log (2 + 2 * M / ρ)) ≤ hullCutConstant ρ * E * (1 + Real.log (2 + M))

theorem TrilinearHT.Auto.dyadicHullFirstCrossingCuts {ι : Type u_1} (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (g : ι → ℝ → ENNReal) (root : ℤ × ℤ) (hHS : ∀ ν ∈ V, H ν ⊆ S) (hS : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) {E M ρ : ℝ} (hE0 : 0 ≤ E) (hM0 : 0 ≤ M) (hρ : 0 < ρ) (hρ1 : ρ < 1) (hE : ∑ ν ∈ V, ∫⁻ (x : ℝ) in dyadicGridCell G root.1 root.2, g ν x ≤ ENNReal.ofReal (E * dyadicGridLength G root.1)) (hM : ∑ ν ∈ V, MeasureTheory.volume (⋃ c ∈ maximalDyadicCells G (H ν), dyadicGridCell G c.1 c.2) ≤ ENNReal.ofReal (M * dyadicGridLength G root.1)) : ∃ C ⊆ S, ((↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2) ∧ dyadicRootLength G C ≤ ρ * dyadicGridLength G root.1 ∧ ∀ (x : ℝ), ∑ ν ∈ V, dyadicHullMax G ({c ∈ H ν | ¬∃ d ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2}) (g ν) x ≤ ENNReal.ofReal (hullCutConstant ρ * E * (1 + Real.log (2 + M)))

Blueprint lem:cuts, hull assertion (eq:hull-cap). For fixed energy densities on finite specified hulls, first-crossing cells of length at most ρ |R| give an everywhere cap Cρ E (1 + log (2 + M)) on whole retained hull cells. Only hull summands are removed; the densities are unchanged.

theorem TrilinearHT.Auto.lintegral_enorm_sq_eq_eLpNorm_sq {F : Type u_1} [NormedAddCommGroup F] (f : ℝ → F) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) : ∫⁻ (x : ℝ), ‖f x‖ₑ ^ 2 = MeasureTheory.eLpNorm f 2 MeasureTheory.volume ^ 2

theorem TrilinearHT.Auto.dyadicHullFirstCrossingCuts_L2 {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] (V : Finset ι) (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (H : ι → Finset (ℤ × ℤ)) (f : ι → ℝ → F) (hf : ∀ ν ∈ V, MeasureTheory.AEStronglyMeasurable (f ν) MeasureTheory.volume) (root : ℤ × ℤ) (hHS : ∀ ν ∈ V, H ν ⊆ S) (hS : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) {E M ρ : ℝ} (hE0 : 0 ≤ E) (hM0 : 0 ≤ M) (hρ : 0 < ρ) (hρ1 : ρ < 1) (hE : ∑ ν ∈ V, MeasureTheory.eLpNorm (f ν) 2 MeasureTheory.volume ^ 2 ≤ ENNReal.ofReal (E * dyadicGridLength G root.1)) (hM : ∑ ν ∈ V, MeasureTheory.volume (⋃ c ∈ maximalDyadicCells G (H ν), dyadicGridCell G c.1 c.2) ≤ ENNReal.ofReal (M * dyadicGridLength G root.1)) : ∃ C ⊆ S, ((↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2) ∧ dyadicRootLength G C ≤ ρ * dyadicGridLength G root.1 ∧ ∀ (x : ℝ), ∑ ν ∈ V, dyadicHullMax G ({c ∈ H ν | ¬∃ d ∈ C, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2}) (fun (y : ℝ) => ‖f ν y‖ₑ ^ 2) x ≤ ENNReal.ofReal (hullCutConstant ρ * E * (1 + Real.log (2 + M)))

The fixed-function L2 version of blueprint lem:cuts: total squared L2 norm and total hull support suffice for the whole-cell retained cap.

noncomputable def TrilinearHT.Auto.dyadicChildren (G : RealDyadicGrid) (c : ℤ × ℤ) : Finset (ℤ × ℤ)

The two children chosen from the grid's exact binary subdivision.

Equations

• TrilinearHT.Auto.dyadicChildren G c = {(c.1 + 1, Classical.choose ⋯), (c.1 + 1, Classical.choose ⋯ + 1)}

theorem TrilinearHT.Auto.dyadicChildren_depth (G : RealDyadicGrid) (c d : ℤ × ℤ) (hd : d ∈ dyadicChildren G c) : d.1 = c.1 + 1

theorem TrilinearHT.Auto.dyadicChildren_subset (G : RealDyadicGrid) (c d : ℤ × ℤ) (hd : d ∈ dyadicChildren G c) : dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G c.1 c.2

theorem TrilinearHT.Auto.dyadicChildren_cover (G : RealDyadicGrid) (c : ℤ × ℤ) {x : ℝ} (hx : x ∈ dyadicGridCell G c.1 c.2) : ∃ d ∈ dyadicChildren G c, x ∈ dyadicGridCell G d.1 d.2

noncomputable def TrilinearHT.Auto.dyadicGeneration (G : RealDyadicGrid) (root : ℤ × ℤ) : ℕ → Finset (ℤ × ℤ)

The complete finite generation below a root cell, used for the terminal completion in blueprint lem:compression, line 553.

Equations

• TrilinearHT.Auto.dyadicGeneration G root 0 = {root}
• TrilinearHT.Auto.dyadicGeneration G root n.succ = (TrilinearHT.Auto.dyadicGeneration G root n).biUnion (TrilinearHT.Auto.dyadicChildren G)

theorem TrilinearHT.Auto.dyadicGeneration_depth (G : RealDyadicGrid) (root : ℤ × ℤ) (n : ℕ) {c : ℤ × ℤ} (hc : c ∈ dyadicGeneration G root n) : c.1 = root.1 + ↑n

theorem TrilinearHT.Auto.dyadicGeneration_subset (G : RealDyadicGrid) (root : ℤ × ℤ) (n : ℕ) {c : ℤ × ℤ} (hc : c ∈ dyadicGeneration G root n) : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2

theorem TrilinearHT.Auto.dyadicGeneration_cover (G : RealDyadicGrid) (root : ℤ × ℤ) (n : ℕ) {x : ℝ} (hx : x ∈ dyadicGridCell G root.1 root.2) : ∃ c ∈ dyadicGeneration G root n, x ∈ dyadicGridCell G c.1 c.2

theorem TrilinearHT.Auto.dyadicGeneration_union (G : RealDyadicGrid) (root : ℤ × ℤ) (n : ℕ) : ⋃ c ∈ dyadicGeneration G root n, dyadicGridCell G c.1 c.2 = dyadicGridCell G root.1 root.2

theorem TrilinearHT.Auto.dyadicGeneration_pairwiseDisjoint (G : RealDyadicGrid) (root : ℤ × ℤ) (n : ℕ) : (↑(dyadicGeneration G root n)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

theorem TrilinearHT.Auto.dyadicGeneration_mem_iff (G : RealDyadicGrid) (root c : ℤ × ℤ) (n : ℕ) : c ∈ dyadicGeneration G root n ↔ c.1 = root.1 + ↑n ∧ dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2

theorem TrilinearHT.Auto.dyadicGridCell_depth_le_of_subset (G : RealDyadicGrid) (c d : ℤ × ℤ) (h : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2) : d.1 ≤ c.1

noncomputable def TrilinearHT.Auto.dyadicFiniteTree (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) : Finset (ℤ × ℤ)

The complete finite tree through generation N, including its root.

Equations

• TrilinearHT.Auto.dyadicFiniteTree G root N = (Finset.range (N + 1)).biUnion (TrilinearHT.Auto.dyadicGeneration G root)

theorem TrilinearHT.Auto.dyadicFiniteTree_mem_iff (G : RealDyadicGrid) (root c : ℤ × ℤ) (N : ℕ) : c ∈ dyadicFiniteTree G root N ↔ dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2 ∧ c.1 ≤ root.1 + ↑N

theorem TrilinearHT.Auto.dyadicFiniteTree_root_mem (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) : root ∈ dyadicFiniteTree G root N

theorem TrilinearHT.Auto.dyadicFiniteTree_ancestor_mem (G : RealDyadicGrid) (root c d : ℤ × ℤ) (N : ℕ) (hc : c ∈ dyadicFiniteTree G root N) (hcd : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2) (hdr : dyadicGridCell G d.1 d.2 ⊆ dyadicGridCell G root.1 root.2) : d ∈ dyadicFiniteTree G root N

theorem TrilinearHT.Auto.dyadicFiniteTree_encloses (G : RealDyadicGrid) (root : ℤ × ℤ) (S : Finset (ℤ × ℤ)) (hS : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) : ∃ (N : ℕ), S ⊆ dyadicFiniteTree G root N ∧ ∀ c ∈ S, c.1 < root.1 + ↑N

Any finite family below a root fits strictly above the terminal generation of a complete finite tree, as required in lem:compression, line 553.

noncomputable def TrilinearHT.Auto.dyadicTerminalCuts (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (B : Finset (ℤ × ℤ)) : Finset (ℤ × ℤ)

Stop at the first marked cells and fill every remaining branch with a terminal leaf. This is the finite cut partition in lem:compression, line 553.

Equations

• TrilinearHT.Auto.dyadicTerminalCuts G root N B = TrilinearHT.Auto.maximalDyadicCells G (B ∪ TrilinearHT.Auto.dyadicGeneration G root N)

theorem TrilinearHT.Auto.dyadicGeneration_subset_finiteTree (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) : dyadicGeneration G root N ⊆ dyadicFiniteTree G root N

theorem TrilinearHT.Auto.dyadicTerminalCuts_subset (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (B : Finset (ℤ × ℤ)) (hB : B ⊆ dyadicFiniteTree G root N) : dyadicTerminalCuts G root N B ⊆ dyadicFiniteTree G root N

theorem TrilinearHT.Auto.dyadicTerminalCuts_pairwiseDisjoint (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (B : Finset (ℤ × ℤ)) : (↑(dyadicTerminalCuts G root N B)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

theorem TrilinearHT.Auto.dyadicTerminalCuts_union (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (B : Finset (ℤ × ℤ)) (hB : B ⊆ dyadicFiniteTree G root N) : ⋃ c ∈ dyadicTerminalCuts G root N B, dyadicGridCell G c.1 c.2 = dyadicGridCell G root.1 root.2

theorem TrilinearHT.Auto.dyadicTerminalCuts_marked_or_terminal (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (B : Finset (ℤ × ℤ)) {c : ℤ × ℤ} (hc : c ∈ dyadicTerminalCuts G root N B) : c ∈ B ∨ c.1 = root.1 + ↑N

theorem TrilinearHT.Auto.dyadicTerminalCuts_ancestor_not_marked (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (B : Finset (ℤ × ℤ)) {c d : ℤ × ℤ} (hc : c ∈ dyadicTerminalCuts G root N B) (hcd : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2) (hne : c ≠ d) : d ∉ B

No proper ancestor of a first cut is marked. In particular its parent satisfies the stopping threshold.

theorem TrilinearHT.Auto.dyadicTerminalCuts_below_unstopped (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (B : Finset (ℤ × ℤ)) {u c : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree G root N) (hstop : ∀ b ∈ B, ¬dyadicGridCell G u.1 u.2 ⊆ dyadicGridCell G b.1 b.2) (hc : c ∈ dyadicTerminalCuts G root N B) {x : ℝ} (hxu : x ∈ dyadicGridCell G u.1 u.2) (hxc : x ∈ dyadicGridCell G c.1 c.2) : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G u.1 u.2

theorem TrilinearHT.Auto.dyadicTerminalCuts_union_below (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (B : Finset (ℤ × ℤ)) (hB : B ⊆ dyadicFiniteTree G root N) {u : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree G root N) (hstop : ∀ b ∈ B, ¬dyadicGridCell G u.1 u.2 ⊆ dyadicGridCell G b.1 b.2) : ⋃ c ∈ {c ∈ dyadicTerminalCuts G root N B | dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G u.1 u.2}, dyadicGridCell G c.1 c.2 = dyadicGridCell G u.1 u.2

The same terminal partition subdivides every cell before the first stop, which is the partition identity needed to preserve its column moments.

noncomputable def TrilinearHT.Auto.dyadicThresholdCells (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (T : ℝ) : Finset (ℤ × ℤ)

Cells whose size exceeds the current segment's threshold.

Equations

• TrilinearHT.Auto.dyadicThresholdCells G root N a T = {c ∈ TrilinearHT.Auto.dyadicFiniteTree G root N | T < a c}

theorem TrilinearHT.Auto.dyadicThresholdCells_subset (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (T : ℝ) : dyadicThresholdCells G root N a T ⊆ dyadicFiniteTree G root N

theorem TrilinearHT.Auto.dyadicThresholdCuts_ancestor_le (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (T : ℝ) {c d : ℤ × ℤ} (hc : c ∈ dyadicTerminalCuts G root N (dyadicThresholdCells G root N a T)) (hd : d ∈ dyadicFiniteTree G root N) (hcd : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2) (hne : c ≠ d) : a d ≤ T

Before the first cut every proper ancestor remains below the threshold. Applying this to the parent is the first half of the four-times-average bound.

theorem TrilinearHT.Auto.dyadicFiniteTree_parent (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) {c : ℤ × ℤ} (hc : c ∈ dyadicFiniteTree G root N) (hne : c ≠ root) : ∃ p ∈ dyadicFiniteTree G root N, c ∈ dyadicChildren G p

Every nonroot cell of a completed finite tree has its parent in that tree.

noncomputable def TrilinearHT.Auto.dyadicCellAverage (G : RealDyadicGrid) (f : ℝ → ℝ) (c : ℤ × ℤ) : ℝ

The normalized average on a dyadic cell; spatial compression applies it to the pointwise norm of the Hilbert-valued input.

Equations

• TrilinearHT.Auto.dyadicCellAverage G f c = (∫ (x : ℝ) in TrilinearHT.Auto.dyadicGridCell G c.1 c.2, f x) / TrilinearHT.Auto.dyadicGridLength G c.1

theorem TrilinearHT.Auto.dyadicCellAverage_nonneg (G : RealDyadicGrid) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), 0 ≤ f x) (c : ℤ × ℤ) : 0 ≤ dyadicCellAverage G f c

theorem TrilinearHT.Auto.dyadicCellAverage_child_le (G : RealDyadicGrid) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), 0 ≤ f x) (p c : ℤ × ℤ) (hc : c ∈ dyadicChildren G p) (hi : MeasureTheory.IntegrableOn f (dyadicGridCell G p.1 p.2) MeasureTheory.volume) : dyadicCellAverage G f c ≤ 2 * dyadicCellAverage G f p

A nonnegative function's child average is at most twice its parent average.

theorem TrilinearHT.Auto.dyadicDoublingCut_average_le (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), 0 ≤ f x) (hi : MeasureTheory.IntegrableOn f (dyadicGridCell G root.1 root.2) MeasureTheory.volume) {c : ℤ × ℤ} (hc : c ∈ dyadicTerminalCuts G root N (dyadicThresholdCells G root N (dyadicCellAverage G f) (2 * dyadicCellAverage G f root))) : dyadicCellAverage G f c ≤ 4 * dyadicCellAverage G f root

Every cut of the doubling-average segment has average at most four times its root average, including terminal leaves (lem:compression, line 553).

theorem TrilinearHT.Auto.dyadicGridCell_depth_lt_of_subset_ne (G : RealDyadicGrid) (c d : ℤ × ℤ) (hsub : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2) (hne : c ≠ d) : d.1 < c.1

noncomputable def TrilinearHT.Auto.dyadicNextSizeRoots (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (K : ℤ × ℤ) : Finset (ℤ × ℤ)

The next roots are the first descendants exceeding twice the current root's size (lem:compression, line 553).

Equations

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

theorem TrilinearHT.Auto.dyadicNextSizeRoots_mem (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (K : ℤ × ℤ) {c : ℤ × ℤ} (hc : c ∈ dyadicNextSizeRoots G S a K) : c ∈ S ∧ dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G K.1 K.2 ∧ 2 * a K < a c

theorem TrilinearHT.Auto.dyadicNextSizeRoots_depth_lt (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (K : ℤ × ℤ) (hK : 0 ≤ a K) {c : ℤ × ℤ} (hc : c ∈ dyadicNextSizeRoots G S a K) : K.1 < c.1

theorem TrilinearHT.Auto.dyadicNextSizeRoots_pairwiseDisjoint (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (K : ℤ × ℤ) : (↑(dyadicNextSizeRoots G S a K)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

noncomputable def TrilinearHT.Auto.dyadicSizeGeneration (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (root : ℤ × ℤ) : ℕ → Finset (ℤ × ℤ)

Stopping generations, indexed by number of average doublings rather than physical depth.

Equations

• TrilinearHT.Auto.dyadicSizeGeneration G S a root 0 = {root}
• TrilinearHT.Auto.dyadicSizeGeneration G S a root n.succ = (TrilinearHT.Auto.dyadicSizeGeneration G S a root n).biUnion (TrilinearHT.Auto.dyadicNextSizeRoots G S a)

theorem TrilinearHT.Auto.dyadicSizeGeneration_subset (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (root : ℤ × ℤ) (hroot : root ∈ S) (n : ℕ) : dyadicSizeGeneration G S a root n ⊆ S

theorem TrilinearHT.Auto.dyadicSizeGeneration_depth (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (root : ℤ × ℤ) (hroot : root ∈ S) (ha : ∀ c ∈ S, 0 ≤ a c) (n : ℕ) {c : ℤ × ℤ} (hc : c ∈ dyadicSizeGeneration G S a root n) : root.1 + ↑n ≤ c.1

theorem TrilinearHT.Auto.dyadicSizeGeneration_pairwiseDisjoint (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (root : ℤ × ℤ) (n : ℕ) : (↑(dyadicSizeGeneration G S a root n)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

theorem TrilinearHT.Auto.dyadicSizeGeneration_eq_empty (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ dyadicFiniteTree G root N, 0 ≤ a c) (n : ℕ) (hn : N < n) : dyadicSizeGeneration G (dyadicFiniteTree G root N) a root n = ∅

Finite physical depth forces termination, without an assumed bound on the number of labels or on the input averages.

noncomputable def TrilinearHT.Auto.dyadicSizeRoots (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) : Finset (ℤ × ℤ)

All stopping roots of the completed finite tree.

Equations

• TrilinearHT.Auto.dyadicSizeRoots G root N a = (Finset.range (N + 1)).biUnion (TrilinearHT.Auto.dyadicSizeGeneration G (TrilinearHT.Auto.dyadicFiniteTree G root N) a root)

theorem TrilinearHT.Auto.dyadicSizeRoots_root_mem (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) : root ∈ dyadicSizeRoots G root N a

theorem TrilinearHT.Auto.dyadicSizeRoots_subset (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) : dyadicSizeRoots G root N a ⊆ dyadicFiniteTree G root N

theorem TrilinearHT.Auto.dyadicSizeRoots_closed (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ dyadicFiniteTree G root N, 0 ≤ a c) {K c : ℤ × ℤ} (hK : K ∈ dyadicSizeRoots G root N a) (hc : c ∈ dyadicNextSizeRoots G (dyadicFiniteTree G root N) a K) : c ∈ dyadicSizeRoots G root N a

noncomputable def TrilinearHT.Auto.dyadicSizeSegment (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (K : ℤ × ℤ) : Finset (ℤ × ℤ)

The cells between a stopping root and its next first crossings.

Equations

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

theorem TrilinearHT.Auto.dyadicSizeSegment_exists (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ dyadicFiniteTree G root N, 0 ≤ a c) {u : ℤ × ℤ} (hu : u ∈ dyadicFiniteTree G root N) : ∃ K ∈ dyadicSizeRoots G root N a, u ∈ dyadicSizeSegment G (dyadicFiniteTree G root N) a K ∧ ∀ L ∈ dyadicSizeRoots G root N a, dyadicGridCell G u.1 u.2 ⊆ dyadicGridCell G L.1 L.2 → L.1 ≤ K.1

Every finite-tree cell belongs to the size segment of a deepest stopping ancestor, exactly as assigned in lem:compression, line 553.

theorem TrilinearHT.Auto.dyadicSizeSegment_no_bad_ancestor (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (K : ℤ × ℤ) {u b : ℤ × ℤ} (hu : u ∈ dyadicSizeSegment G S a K) (hb : b ∈ S) (hbK : dyadicGridCell G b.1 b.2 ⊆ dyadicGridCell G K.1 K.2) (hbad : 2 * a K < a b) : ¬dyadicGridCell G u.1 u.2 ⊆ dyadicGridCell G b.1 b.2

No threshold-violating ancestor occurs between a segment cell and its root.

def TrilinearHT.Auto.dyadicRemainingDepth (root : ℤ × ℤ) (N : ℕ) (K : ℤ × ℤ) : ℕ

The physical generations remaining below a cell in the completed tree.

Equations

• TrilinearHT.Auto.dyadicRemainingDepth root N K = (root.1 + ↑N - K.1).toNat

theorem TrilinearHT.Auto.dyadicRemainingDepth_endpoint (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) {K : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree G root N) : K.1 + ↑(dyadicRemainingDepth root N K) = root.1 + ↑N

theorem TrilinearHT.Auto.dyadicFiniteTree_below_iff (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) {K : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree G root N) (c : ℤ × ℤ) : c ∈ dyadicFiniteTree G K (dyadicRemainingDepth root N K) ↔ c ∈ dyadicFiniteTree G root N ∧ dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G K.1 K.2

noncomputable def TrilinearHT.Auto.dyadicSizeSegmentCuts (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (K : ℤ × ℤ) : Finset (ℤ × ℤ)

The first crossings and terminal leaves form the cut partition of a size segment.

Equations

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

theorem TrilinearHT.Auto.dyadicSizeSegmentCuts_subset (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) {K : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree G root N) : dyadicSizeSegmentCuts G root N a K ⊆ dyadicFiniteTree G root N

theorem TrilinearHT.Auto.dyadicSizeSegmentCuts_union (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (K : ℤ × ℤ) : ⋃ c ∈ dyadicSizeSegmentCuts G root N a K, dyadicGridCell G c.1 c.2 = dyadicGridCell G K.1 K.2

theorem TrilinearHT.Auto.dyadicSizeSegmentCuts_pairwiseDisjoint (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (K : ℤ × ℤ) : (↑(dyadicSizeSegmentCuts G root N a K)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

theorem TrilinearHT.Auto.dyadicSizeSegmentCuts_union_below (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) {K u : ℤ × ℤ} (hK : K ∈ dyadicFiniteTree G root N) (hu : u ∈ dyadicSizeSegment G (dyadicFiniteTree G root N) a K) : ⋃ c ∈ {c ∈ dyadicSizeSegmentCuts G root N a K | dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G u.1 u.2}, dyadicGridCell G c.1 c.2 = dyadicGridCell G u.1 u.2

Every row cell assigned to a segment is exactly the union of the cuts below it, the geometric identity behind preserved moments.

theorem TrilinearHT.Auto.dyadicHullMax_weak_local (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (g : ℝ → ENNReal) (t : ENNReal) : t * MeasureTheory.volume {x : ℝ | t < dyadicHullMax G S g x} ≤ ∫⁻ (x : ℝ) in {y : ℝ | t < dyadicHullMax G S g y}, g x

The sharp local weak estimate integrates the density over the very same superlevel set. This is the distribution estimate behind the dyadic L2 bound.

theorem TrilinearHT.Auto.maximal_layercake_energy {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (M : α → ℝ) (g : α → ENNReal) (hM : Measurable M) (hM0 : ∀ (x : α), 0 ≤ M x) (hg : Measurable g) (hweak : ∀ (t : ℝ), 0 < t → ENNReal.ofReal t * μ {x : α | t < M x} ≤ ∫⁻ (x : α) in {y : α | t < M y}, g x ∂μ) : ∫⁻ (x : α), ENNReal.ofReal (M x ^ 2) ∂μ ≤ 2 * ∫⁻ (x : α), g x * ENNReal.ofReal (M x) ∂μ

The layer-cake step in the classical maximal L2 proof: a local weak-type estimate gives the energy bound integral M² ≤ 2 integral g M. The density may be extended-valued; finiteness is required only in the later cancellation.

theorem TrilinearHT.Auto.dyadicEnergyAverage_ofReal (G : RealDyadicGrid) (f : ℝ → ℝ) (c : ℤ × ℤ) (hf : ∀ (x : ℝ), 0 ≤ f x) (hi : MeasureTheory.IntegrableOn f (dyadicGridCell G c.1 c.2) MeasureTheory.volume) : dyadicEnergyAverage G (fun (x : ℝ) => ENNReal.ofReal (f x)) c = ENNReal.ofReal (dyadicCellAverage G f c)

noncomputable def TrilinearHT.Auto.dyadicRealMax (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℝ → ℝ) (x : ℝ) : ℝ

The ordinary finite dyadic maximal function of a nonnegative density.

Equations

• TrilinearHT.Auto.dyadicRealMax G S f x = (TrilinearHT.Auto.dyadicHullMax G S (fun (y : ℝ) => ENNReal.ofReal (f y)) x).toReal

theorem TrilinearHT.Auto.dyadicRealMax_measurable (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℝ → ℝ) : Measurable (dyadicRealMax G S f)

theorem TrilinearHT.Auto.dyadicRealMax_nonneg (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℝ → ℝ) (x : ℝ) : 0 ≤ dyadicRealMax G S f x

theorem TrilinearHT.Auto.dyadicHullMax_ofReal_le_sum (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), 0 ≤ f x) (hi : ∀ c ∈ S, MeasureTheory.IntegrableOn f (dyadicGridCell G c.1 c.2) MeasureTheory.volume) (x : ℝ) : dyadicHullMax G S (fun (y : ℝ) => ENNReal.ofReal (f y)) x ≤ ENNReal.ofReal (∑ c ∈ S, dyadicCellAverage G f c)

theorem TrilinearHT.Auto.dyadicRealMax_ofReal (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), 0 ≤ f x) (hi : ∀ c ∈ S, MeasureTheory.IntegrableOn f (dyadicGridCell G c.1 c.2) MeasureTheory.volume) (x : ℝ) : ENNReal.ofReal (dyadicRealMax G S f x) = dyadicHullMax G S (fun (y : ℝ) => ENNReal.ofReal (f y)) x

theorem TrilinearHT.Auto.dyadicRealMax_le_sum (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), 0 ≤ f x) (hi : ∀ c ∈ S, MeasureTheory.IntegrableOn f (dyadicGridCell G c.1 c.2) MeasureTheory.volume) (x : ℝ) : dyadicRealMax G S f x ≤ ∑ c ∈ S, dyadicCellAverage G f c

theorem TrilinearHT.Auto.dyadicRealMax_eq_zero_off (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℝ → ℝ) (root : ℤ × ℤ) (hS : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) {x : ℝ} (hx : x ∉ dyadicGridCell G root.1 root.2) : dyadicRealMax G S f x = 0

theorem TrilinearHT.Auto.dyadicRealMax_memLp (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), 0 ≤ f x) (hi : ∀ c ∈ S, MeasureTheory.IntegrableOn f (dyadicGridCell G c.1 c.2) MeasureTheory.volume) (root : ℤ × ℤ) (hS : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) : MeasureTheory.MemLp (dyadicRealMax G S f) 2 MeasureTheory.volume

theorem TrilinearHT.Auto.maximal_layercake_l2 {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (M f : α → ℝ) (hM : Measurable M) (hf : Measurable f) (hM0 : ∀ (x : α), 0 ≤ M x) (hf0 : ∀ (x : α), 0 ≤ f x) (hM2 : MeasureTheory.MemLp M 2 μ) (hf2 : MeasureTheory.MemLp f 2 μ) (hweak : ∀ (t : ℝ), 0 < t → ENNReal.ofReal t * μ {x : α | t < M x} ≤ ∫⁻ (x : α) in {y : α | t < M y}, ENNReal.ofReal (f x) ∂μ) : ∫ (x : α), M x ^ 2 ∂μ ≤ 4 * ∫ (x : α), f x ^ 2 ∂μ

Cauchy–Schwarz closes the weighted maximal energy estimate with the sharp L2 norm constant two (squared constant four). Finiteness is supplied explicitly by the two MemLp hypotheses before any cancellation is made.

theorem TrilinearHT.Auto.dyadicRealMax_l2 (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (root : ℤ × ℤ) (hS : ∀ c ∈ S, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2) (f : ℝ → ℝ) (hf : Measurable f) (hf0 : ∀ (x : ℝ), 0 ≤ f x) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ∫ (x : ℝ), dyadicRealMax G S f x ^ 2 ≤ 4 * ∫ (x : ℝ), f x ^ 2

The finite dyadic maximal operator has squared L2 bound four, hence L2 norm bound two, uniformly in the number of cells and physical depth.

theorem TrilinearHT.Auto.dyadicCellAverage_le_max (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℝ → ℝ) (hf : ∀ (x : ℝ), 0 ≤ f x) (hi : ∀ c ∈ S, MeasureTheory.IntegrableOn f (dyadicGridCell G c.1 c.2) MeasureTheory.volume) {c : ℤ × ℤ} (hc : c ∈ S) {x : ℝ} (hx : x ∈ dyadicGridCell G c.1 c.2) : dyadicCellAverage G f c ≤ dyadicRealMax G S f x

theorem TrilinearHT.Auto.dyadicSizeGeneration_ancestor (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (root : ℤ × ℤ) (hroot : root ∈ S) (ha : ∀ c ∈ S, 0 ≤ a c) (i j : ℕ) (hij : i ≤ j) {L : ℤ × ℤ} (hL : L ∈ dyadicSizeGeneration G S a root j) : ∃ K ∈ dyadicSizeGeneration G S a root i, dyadicGridCell G L.1 L.2 ⊆ dyadicGridCell G K.1 K.2 ∧ a K ≤ a L ∧ (i < j → 2 * a K < a L)

Every later stopping root descends from a root of each earlier stopping generation, and its size has increased by at least one doubling.

theorem TrilinearHT.Auto.dyadicSizeGeneration_sameLevel_common_point (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (a : ℤ × ℤ → ℝ) (root : ℤ × ℤ) (n : ℕ) {K L : ℤ × ℤ} (hK : K ∈ dyadicSizeGeneration G S a root n) (hL : L ∈ dyadicSizeGeneration G S a root n) {x : ℝ} (hxK : x ∈ dyadicGridCell G K.1 K.2) (hxL : x ∈ dyadicGridCell G L.1 L.2) : K = L

theorem TrilinearHT.Auto.dyadicSizeRoots_nested_doubling (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ dyadicFiniteTree G root N, 0 ≤ a c) {K L : ℤ × ℤ} (hK : K ∈ dyadicSizeRoots G root N a) (hL : L ∈ dyadicSizeRoots G root N a) (hLK : dyadicGridCell G L.1 L.2 ⊆ dyadicGridCell G K.1 K.2) (hne : L ≠ K) : 2 * a K < a L

Distinct nested stopping roots have strictly doubled sizes, even when their stopping generations are not consecutive.

theorem TrilinearHT.Auto.finite_doubling_square_sum_le {ι : Type u_1} (S : Finset ι) (a : ι → ℝ) (ha : ∀ i ∈ S, 0 ≤ a i) (hsep : ∀ i ∈ S, ∀ j ∈ S, i ≠ j → 2 * a i ≤ a j ∨ 2 * a j ≤ a i) (M : ℝ) (hM0 : 0 ≤ M) (hM : ∀ i ∈ S, a i ≤ M) : ∑ i ∈ S, a i ^ 2 ≤ 4 / 3 * M ^ 2

A finite geometrically separated family of nonnegative sizes has square sum at most four thirds of the square of any common upper bound.

theorem TrilinearHT.Auto.dyadicSizeRoots_square_path_le (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ dyadicFiniteTree G root N, 0 ≤ a c) (x M : ℝ) (hM0 : 0 ≤ M) (hM : ∀ c ∈ dyadicFiniteTree G root N, x ∈ dyadicGridCell G c.1 c.2 → a c ≤ M) : dyadicRealPathSum G (dyadicSizeRoots G root N a) (fun (c : ℤ × ℤ) => a c ^ 2) x ≤ 4 / 3 * M ^ 2

Blueprint lem:compression, lines 561–564: the squared stopping sizes on a path form a geometric series with exact constant four thirds.

theorem TrilinearHT.Auto.finite_doubling_sum_le {ι : Type u_1} (S : Finset ι) (a : ι → ℝ) (ha : ∀ i ∈ S, 0 ≤ a i) (hsep : ∀ i ∈ S, ∀ j ∈ S, i ≠ j → 2 * a i ≤ a j ∨ 2 * a j ≤ a i) (M : ℝ) (hM0 : 0 ≤ M) (hM : ∀ i ∈ S, a i ≤ M) : ∑ i ∈ S, a i ≤ 2 * M

Small geometrically separated sizes have total at most twice their common upper bound, the small-size estimate in lem:compression, line 565.

theorem TrilinearHT.Auto.finite_doubling_card_power_le {ι : Type u_1} (S : Finset ι) (a : ι → ℝ) (hS : S.Nonempty) (hsep : ∀ i ∈ S, ∀ j ∈ S, i ≠ j → 2 * a i ≤ a j ∨ 2 * a j ≤ a i) (m M : ℝ) (hm : 0 < m) (hlo : ∀ i ∈ S, m ≤ a i) (hhi : ∀ i ∈ S, a i ≤ M) : 2 ^ (S.card - 1) * m ≤ M

A nonempty separated family with positive lower size has exponentially large top size as a function of its cardinality.

theorem TrilinearHT.Auto.finite_doubling_card_le_logb {ι : Type u_1} (S : Finset ι) (a : ι → ℝ) (hsep : ∀ i ∈ S, ∀ j ∈ S, i ≠ j → 2 * a i ≤ a j ∨ 2 * a j ≤ a i) (m M : ℝ) (hm : 0 < m) (hmM : m ≤ M) (hlo : ∀ i ∈ S, m ≤ a i) (hhi : ∀ i ∈ S, a i ≤ M) : ↑S.card ≤ 1 + Real.logb 2 (M / m)

The number of geometrically separated sizes in [m,M] is at most one plus the base-two logarithm of M/m.

theorem TrilinearHT.Auto.finite_doubling_card_le_ceil_logb {ι : Type u_1} (S : Finset ι) (a : ι → ℝ) (hsep : ∀ i ∈ S, ∀ j ∈ S, i ≠ j → 2 * a i ≤ a j ∨ 2 * a j ≤ a i) (m M : ℝ) (hm : 0 < m) (hmM : m ≤ M) (hlo : ∀ i ∈ S, m ≤ a i) (hhi : ∀ i ∈ S, a i ≤ M) : S.card ≤ 1 + ⌈Real.logb 2 (M / m)⌉₊

theorem TrilinearHT.Auto.dyadicSizeRoots_path_separation (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ dyadicFiniteTree G root N, 0 ≤ a c) {c d : ℤ × ℤ} (hc : c ∈ dyadicSizeRoots G root N a) (hd : d ∈ dyadicSizeRoots G root N a) {x : ℝ} (hxc : x ∈ dyadicGridCell G c.1 c.2) (hxd : x ∈ dyadicGridCell G d.1 d.2) (hne : c ≠ d) : 2 * a c < a d ∨ 2 * a d < a c

noncomputable def TrilinearHT.Auto.dyadicSmallSizeRoots (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (x T : ℝ) : Finset (ℤ × ℤ)

Size-stopping roots containing x with weight below T.

Equations

• TrilinearHT.Auto.dyadicSmallSizeRoots G root N a x T = {K ∈ TrilinearHT.Auto.dyadicSizeRoots G root N a | x ∈ TrilinearHT.Auto.dyadicGridCell G K.1 K.2 ∧ a K < T}

noncomputable def TrilinearHT.Auto.dyadicLargeSizeRoots (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (x T : ℝ) : Finset (ℤ × ℤ)

Size-stopping roots containing x with weight at least T.

Equations

• TrilinearHT.Auto.dyadicLargeSizeRoots G root N a x T = {K ∈ TrilinearHT.Auto.dyadicSizeRoots G root N a | x ∈ TrilinearHT.Auto.dyadicGridCell G K.1 K.2 ∧ T ≤ a K}

theorem TrilinearHT.Auto.dyadicSmallSizeRoots_sum_le (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ dyadicFiniteTree G root N, 0 ≤ a c) (x T : ℝ) (hT : 0 ≤ T) : ∑ K ∈ dyadicSmallSizeRoots G root N a x T, a K ≤ 2 * T

theorem TrilinearHT.Auto.dyadicLargeSizeRoots_card_le (G : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ dyadicFiniteTree G root N, 0 ≤ a c) (x M Q : ℝ) (hM0 : 0 ≤ M) (hQ : 1 ≤ Q) (hM : ∀ c ∈ dyadicFiniteTree G root N, x ∈ dyadicGridCell G c.1 c.2 → a c ≤ M) : (dyadicLargeSizeRoots G root N a x (M / Q)).card ≤ 1 + ⌈Real.logb 2 Q⌉₊

At most 1 + ceil(log₂ Q) stopping roots on a path have size at least M/Q, provided all sizes are at most M. At M = 0, strict separation leaves at most one root, so no division by the maximum is assumed.

noncomputable def TrilinearHT.Auto.dyadicLogSizeCount (Q : ℝ) : ℕ

The logarithmic overlap count used for the large stopping sizes.

Equations

• TrilinearHT.Auto.dyadicLogSizeCount Q = 2 + ⌈Real.logb 2 Q⌉₊

theorem TrilinearHT.Auto.finite_sum_le_sqrt_card_sq_sum {ι : Type u_1} (S : Finset ι) (b : ι → ℝ) : ∑ i ∈ S, b i ≤ √↑S.card * √(∑ i ∈ S, b i ^ 2)

theorem TrilinearHT.Auto.dyadic_stopped_values_sum_bound (grid : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a b : ℤ × ℤ → ℝ) (ha : ∀ c ∈ dyadicFiniteTree grid root N, 0 ≤ a c) (x M G Q : ℝ) (hM0 : 0 ≤ M) (hG : 0 ≤ G) (hQ : 1 ≤ Q) (hM : ∀ c ∈ dyadicFiniteTree grid root N, x ∈ dyadicGridCell grid c.1 c.2 → a c ≤ M) (hb0 : ∀ c ∈ dyadicSizeRoots grid root N a, x ∉ dyadicGridCell grid c.1 c.2 → b c = 0) (hb : ∀ c ∈ dyadicSizeRoots grid root N a, x ∈ dyadicGridCell grid c.1 c.2 → b c ≤ G * a c) : ∑ c ∈ dyadicSizeRoots grid root N a, b c ≤ 2 * G / Q * M + √↑(dyadicLogSizeCount Q) * √(∑ c ∈ dyadicSizeRoots grid root N a, b c ^ 2)

The small/large size split bounds any nonnegative supported values with amplitude at most G a_K; only a logarithmic overlap loss remains.

theorem TrilinearHT.Auto.complexLp_norm_sq_integral {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℂ E] (μ : MeasureTheory.Measure α) (z : ↥(MeasureTheory.Lp E 2 μ)) : ‖z‖ ^ 2 = ∫ (x : α), ‖↑↑z x‖ ^ 2 ∂μ

theorem TrilinearHT.Auto.realLp_norm_sq_integral {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (z : ↥(MeasureTheory.Lp ℝ 2 μ)) : ‖z‖ ^ 2 = ∫ (x : α), ↑↑z x ^ 2 ∂μ

theorem TrilinearHT.Auto.finite_L2_sum_norm_bound {α : Type u_1} {E : Type u_2} {ι : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℂ E] (μ : MeasureTheory.Measure α) (S : Finset ι) (g : ι → ↥(MeasureTheory.Lp E 2 μ)) (M : α → ℝ) (hM : MeasureTheory.MemLp M 2 μ) (hM0 : ∀ (x : α), 0 ≤ M x) (c L : ℝ) (hc : 0 ≤ c) (hL : 0 ≤ L) (hbound : ∀ᵐ (x : α) ∂μ, ∑ i ∈ S, ‖↑↑(g i) x‖ ≤ c * M x + L * √(∑ i ∈ S, ‖↑↑(g i) x‖ ^ 2)) : ‖∑ i ∈ S, g i‖ ≤ c * √(∫ (x : α), M x ^ 2 ∂μ) + L * √(∑ i ∈ S, ‖g i‖ ^ 2)

Transfer a pointwise finite-family bound to its L2 sum. The square function has squared L2 norm exactly equal to the sum of the individual energies.

theorem TrilinearHT.Auto.dyadic_stopped_moment_energy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (grid : RealDyadicGrid) (root : ℤ × ℤ) (N : ℕ) (a : ℤ × ℤ → ℝ) (ha : ∀ c ∈ dyadicFiniteTree grid root N, 0 ≤ a c) (z : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (g : ℤ × ℤ → ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (M : ℝ → ℝ) (hM2 : MeasureTheory.MemLp M 2 MeasureTheory.volume) (hM0 : ∀ (x : ℝ), 0 ≤ M x) (G Q : ℝ) (hG : 0 ≤ G) (hQ : 1 ≤ Q) (hM : ∀ (x : ℝ), ∀ c ∈ dyadicFiniteTree grid root N, x ∈ dyadicGridCell grid c.1 c.2 → a c ≤ M x) (hzero : ∀ c ∈ dyadicSizeRoots grid root N a, ∀ᵐ (x : ℝ), x ∉ dyadicGridCell grid c.1 c.2 → ↑↑(g c) x = 0) (hbound : ∀ c ∈ dyadicSizeRoots grid root N a, ∀ᵐ (x : ℝ), ‖↑↑(g c) x‖ ≤ G * a c) (henergy : ∀ c ∈ dyadicSizeRoots grid root N a, ‖g c‖ ^ 2 = (inner ℂ z (g c)).re) : ∑ c ∈ dyadicSizeRoots grid root N a, ‖g c‖ ^ 2 ≤ 2 * G / Q * ‖z‖ * √(∫ (x : ℝ), M x ^ 2) + √↑(dyadicLogSizeCount Q) * ‖z‖ * √(∑ c ∈ dyadicSizeRoots grid root N a, ‖g c‖ ^ 2)

The abstract logarithmic moment-energy inequality from lem:compression, line 565. Support, pointwise amplitude bounds and projection moment identities are explicit hypotheses; no size of the entire root family appears in the bound.

noncomputable def TrilinearHT.Auto.dyadicNextAnchors {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (K : ℤ × ℤ) : Finset (ℤ × ℤ)

First descendants whose coefficient displacement from the preceding anchor exceeds a fixed tolerance (lem:compression, line 567).

Equations

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

theorem TrilinearHT.Auto.dyadicNextAnchors_mem {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (K : ℤ × ℤ) {c : ℤ × ℤ} (hc : c ∈ dyadicNextAnchors G S f t K) : c ∈ S ∧ dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G K.1 K.2 ∧ t < ‖f c - f K‖

theorem TrilinearHT.Auto.dyadicNextAnchors_depth_lt {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (ht : 0 ≤ t) (K : ℤ × ℤ) {c : ℤ × ℤ} (hc : c ∈ dyadicNextAnchors G S f t K) : K.1 < c.1

theorem TrilinearHT.Auto.dyadicNextAnchors_pairwiseDisjoint {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (K : ℤ × ℤ) : (↑(dyadicNextAnchors G S f t K)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

noncomputable def TrilinearHT.Auto.dyadicAnchorGeneration {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) : ℕ → Finset (ℤ × ℤ)

Generations count coefficient transitions, independently of spatial depth.

Equations

• TrilinearHT.Auto.dyadicAnchorGeneration G S f t root 0 = {root}
• TrilinearHT.Auto.dyadicAnchorGeneration G S f t root n.succ = (TrilinearHT.Auto.dyadicAnchorGeneration G S f t root n).biUnion (TrilinearHT.Auto.dyadicNextAnchors G S f t)

theorem TrilinearHT.Auto.dyadicAnchorGeneration_subset {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (hroot : root ∈ S) (n : ℕ) : dyadicAnchorGeneration G S f t root n ⊆ S

theorem TrilinearHT.Auto.dyadicAnchorGeneration_depth {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (ht : 0 ≤ t) (root : ℤ × ℤ) (n : ℕ) {c : ℤ × ℤ} (hc : c ∈ dyadicAnchorGeneration G S f t root n) : root.1 + ↑n ≤ c.1

theorem TrilinearHT.Auto.dyadicAnchorGeneration_below {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (n : ℕ) {c : ℤ × ℤ} (hc : c ∈ dyadicAnchorGeneration G S f t root n) : dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G root.1 root.2

theorem TrilinearHT.Auto.dyadicAnchorGeneration_pairwiseDisjoint {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (n : ℕ) : (↑(dyadicAnchorGeneration G S f t root n)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

noncomputable def TrilinearHT.Auto.dyadicAnchorSegment {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (K : ℤ × ℤ) : Finset (ℤ × ℤ)

Cells assigned to one anchor before its next coefficient crossing.

Equations

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

theorem TrilinearHT.Auto.dyadicAnchorSegment_error_le {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (K : ℤ × ℤ) {u : ℤ × ℤ} (hu : u ∈ dyadicAnchorSegment G S f t K) : ‖f u - f K‖ ≤ t

theorem TrilinearHT.Auto.dyadicAnchorGeneration_assignment {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) {u : ℤ × ℤ} (hu : u ∈ S) (hur : dyadicGridCell G u.1 u.2 ⊆ dyadicGridCell G root.1 root.2) (T : ℕ) : (∃ R ∈ dyadicAnchorGeneration G S f t root T, dyadicGridCell G u.1 u.2 ⊆ dyadicGridCell G R.1 R.2) ∨ ∃ j < T, ∃ K ∈ dyadicAnchorGeneration G S f t root j, u ∈ dyadicAnchorSegment G S f t K

After any prescribed number of transitions a cell either lies under a restart root or has a last anchor of smaller generation, with controlled error. No assumption on spatial depth or on the coefficient space dimension is used.

theorem TrilinearHT.Auto.dyadicAnchorGeneration_add {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (n k : ℕ) : dyadicAnchorGeneration G S f t root (n + k) = (dyadicAnchorGeneration G S f t root n).biUnion fun (K : ℤ × ℤ) => dyadicAnchorGeneration G S f t K k

Restarting the same coefficient rule loses no transitions: generations compose exactly, with the original coefficient function and tolerance.

noncomputable def TrilinearHT.Auto.dyadicRestartGeneration {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (T n : ℕ) : Finset (ℤ × ℤ)

Attempt roots are every Tth coefficient-anchor generation.

Equations

• TrilinearHT.Auto.dyadicRestartGeneration G S f t root T n = TrilinearHT.Auto.dyadicAnchorGeneration G S f t root (n * T)

theorem TrilinearHT.Auto.dyadicRestartGeneration_succ {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (T n : ℕ) : dyadicRestartGeneration G S f t root T (n + 1) = (dyadicRestartGeneration G S f t root T n).biUnion fun (R : ℤ × ℤ) => dyadicAnchorGeneration G S f t R T

theorem TrilinearHT.Auto.dyadicAnchorGeneration_retained_assignment {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) {u : ℤ × ℤ} (hu : u ∈ S) (hur : dyadicGridCell G u.1 u.2 ⊆ dyadicGridCell G root.1 root.2) (T : ℕ) (hretain : ∀ R ∈ dyadicAnchorGeneration G S f t root T, ¬dyadicGridCell G u.1 u.2 ⊆ dyadicGridCell G R.1 R.2) : ∃ j < T, ∃ K ∈ dyadicAnchorGeneration G S f t root j, u ∈ dyadicAnchorSegment G S f t K ∧ ‖f u - f K‖ ≤ t

A finite attempt assigns every non-restarted cell to a spatial anchor generation below T, and the coefficient error is at most t.

noncomputable def TrilinearHT.Auto.dyadicAnchorCuts {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (N n : ℕ) : Finset (ℤ × ℤ)

Complete an anchor generation by retaining terminal leaves on branches with no anchor at that generation (lem:compression, line 569).

Equations

• TrilinearHT.Auto.dyadicAnchorCuts G S f t root N n = TrilinearHT.Auto.dyadicTerminalCuts G root N (TrilinearHT.Auto.dyadicAnchorGeneration G S f t root n)

theorem TrilinearHT.Auto.dyadicAnchorGeneration_subset_localTree {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (N : ℕ) (hroot : root ∈ S) (hdepth : ∀ c ∈ S, c.1 ≤ root.1 + ↑N) (n : ℕ) : dyadicAnchorGeneration G S f t root n ⊆ dyadicFiniteTree G root N

theorem TrilinearHT.Auto.dyadicAnchorCuts_subset {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (N : ℕ) (hroot : root ∈ S) (hdepth : ∀ c ∈ S, c.1 ≤ root.1 + ↑N) (n : ℕ) : dyadicAnchorCuts G S f t root N n ⊆ dyadicFiniteTree G root N

theorem TrilinearHT.Auto.dyadicAnchorCuts_pairwiseDisjoint {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (N n : ℕ) : (↑(dyadicAnchorCuts G S f t root N n)).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2

theorem TrilinearHT.Auto.dyadicAnchorCuts_union {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (N : ℕ) (hroot : root ∈ S) (hdepth : ∀ c ∈ S, c.1 ≤ root.1 + ↑N) (n : ℕ) : ⋃ c ∈ dyadicAnchorCuts G S f t root N n, dyadicGridCell G c.1 c.2 = dyadicGridCell G root.1 root.2

theorem TrilinearHT.Auto.dyadicAnchorCuts_anchor_mem {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (N : ℕ) (hroot : root ∈ S) (hdepth : ∀ c ∈ S, c.1 ≤ root.1 + ↑N) (n : ℕ) {b : ℤ × ℤ} (hb : b ∈ dyadicAnchorGeneration G S f t root n) : b ∈ dyadicAnchorCuts G S f t root N n

Every genuine anchor is an atom of the completed stopping partition; terminal completion does not discard or enlarge its cell.

theorem TrilinearHT.Auto.dyadicAnchorCuts_refines {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) (N : ℕ) {n k : ℕ} (hnk : n ≤ k) {c : ℤ × ℤ} (hc : c ∈ dyadicAnchorCuts G S f t root N k) : ∃ d ∈ dyadicAnchorCuts G S f t root N n, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2

Completed anchor partitions refine with the transition index, including the terminal atoms that have already stopped changing.

theorem TrilinearHT.Auto.dyadicPartition_refinement_cover (G : RealDyadicGrid) (B C : Finset (ℤ × ℤ)) (R : Set ℝ) (hB : (↑B).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2) (hC : ⋃ c ∈ C, dyadicGridCell G c.1 c.2 = R) (href : ∀ c ∈ C, ∃ d ∈ B, dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G d.1 d.2) {b : ℤ × ℤ} (hb : b ∈ B) (hbR : dyadicGridCell G b.1 b.2 ⊆ R) : ⋃ c ∈ {c ∈ C | dyadicGridCell G c.1 c.2 ⊆ dyadicGridCell G b.1 b.2}, dyadicGridCell G c.1 c.2 = dyadicGridCell G b.1 b.2

Refinement of two finite partitions restricts to an exact partition of each old atom. This supplies the local range-inclusion argument.

theorem TrilinearHT.Auto.dyadicAnchorGeneration_jump_ancestors {E : Type u_1} [NormedAddCommGroup E] (G : RealDyadicGrid) (S : Finset (ℤ × ℤ)) (f : ℤ × ℤ → E) (t : ℝ) (root : ℤ × ℤ) {T n : ℕ} (hn : n < T) {r : ℤ × ℤ} (hr : r ∈ dyadicAnchorGeneration G S f t root T) : ∃ K ∈ dyadicAnchorGeneration G S f t root n, ∃ c ∈ dyadicNextAnchors G S f t K, dyadicGridCell G r.1 r.2 ⊆ dyadicGridCell G c.1 c.2

A restart root lies under one genuine transition at every earlier anchor generation (lem:compression, lines 569–572).

theorem TrilinearHT.Auto.dyadic_disjoint_mass_le_L2_energy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (G : RealDyadicGrid) (C : Finset (ℤ × ℤ)) (hdis : (↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2) (z : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (δ : ℝ) (hδ : 0 ≤ δ) (hbound : ∀ᵐ (x : ℝ), ∀ c ∈ C, x ∈ dyadicGridCell G c.1 c.2 → δ ≤ ‖↑↑z x‖) : δ ^ 2 * ∑ c ∈ C, dyadicGridLength G c.1 ≤ ‖z‖ ^ 2

A uniform norm lower bound on a finite disjoint dyadic family charges its total length to the L2 energy of the same function.

theorem TrilinearHT.Auto.dyadic_jump_mass_le_energy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (G : RealDyadicGrid) (C : Finset (ℤ × ℤ)) (hdis : (↑C).PairwiseDisjoint fun (c : ℤ × ℤ) => dyadicGridCell G c.1 c.2) (T : ℕ) (u : Fin T → ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (δ : ℝ) (hδ : 0 ≤ δ) (hbound : ∀ (n : Fin T), ∀ᵐ (x : ℝ), ∀ c ∈ C, x ∈ dyadicGridCell G c.1 c.2 → δ ≤ ‖↑↑(u n) x‖) : ↑T * δ ^ 2 * ∑ c ∈ C, dyadicGridLength G c.1 ≤ ∑ n : Fin T, ‖u n‖ ^ 2

Integrating every transition lower bound over the same disjoint restart roots gives the factor T in the source restart budget.

theorem TrilinearHT.Auto.restart_weight_packing {α : Type u_1} [DecidableEq α] (root : α) (generation : ℕ → Finset α) (children : ℕ → α → Finset α) (w : α → ℝ) (hw : ∀ (x : α), 0 ≤ w x) {ρ : ℝ} (hρ : 0 ≤ ρ) (hρ1 : ρ < 1) (hzero : generation 0 = {root}) (hnext : ∀ (n : ℕ), generation (n + 1) ⊆ (generation n).biUnion (children n)) (hchild : ∀ (n : ℕ), ∀ c ∈ generation n, ∑ d ∈ children n c, w d ≤ ρ * w c) : (Summable fun (n : ℕ) => ∑ c ∈ generation n, w c) ∧ ∑' (n : ℕ), ∑ c ∈ generation n, w c ≤ w root / (1 - ρ)

The geometric restart argument for arbitrary nonnegative root costs, so the same proof applies to both length and restricted L2 energy.