Section 11.1: Two structured inputs and delayed moments (part 1b: lem:delay)

This file was automatically generated by Claude.

Formalization of blueprint Section 11, "The base reduction" (sec:base), subsection 1, "Two structured inputs and delayed moments", part 1b: lem:delay (lines 1536-1568) of blueprint/formalization_blueprint.tex.

theorem TrilinearHT.Auto.cellColumnProjection_norm_le {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {c : ℤ × ℤ} (hc : c ∈ D.cells) : ‖cellColumnProjection D A hc‖ ≤ 1

theorem TrilinearHT.Auto.partitionColumnProjection_nested {V : Type u_1} [Fintype V] (D : ColumnTreeData V) (A : InheritedColumnMask D) {σ π : ColumnStoppingPartition D} (href : ColumnPartitionRefines σ π) : partitionColumnProjection D A π ∘SL partitionColumnProjection D A σ = partitionColumnProjection D A π

The orthogonal projections on refining stopping partitions are nested; this is derived from the inherited masks, not assumed in the interface.

theorem TrilinearHT.Auto.delay_cell_telescope (G : RealDyadicGrid) (I : ℤ × ℤ) {θ : ℝ → ℂ} {L : ℝ} (hL : 0 ≤ L) (hθc : Continuous θ) (hθb : ∀ (y : ℝ), ‖θ y‖ ≤ L) (hLip : ∀ (y z : ℝ), ‖θ y - θ z‖ ≤ L / dyadicGridLength G I.1 * |y - z|) (D μ : ℕ → ℝ → ℂ) (hD2 : ∀ (j : ℕ), MeasureTheory.MemLp (D j) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (hμ2 : ∀ (j : ℕ), MeasureTheory.MemLp (μ j) 2 (MeasureTheory.volume.restrict (dyadicGridCell G I.1 I.2))) (n d : ℕ) (hμc : ∀ j ≤ n + d, ∀ Q ∈ dyadicGeneration G I j, ∀ y ∈ dyadicGridCell G Q.1 Q.2, ∀ z ∈ dyadicGridCell G Q.1 Q.2, μ j y = μ j z) (hDμ : ∀ j ≤ n + d, ∀ Q ∈ dyadicGeneration G I j, ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, D j y = ∫ (y : ℝ) in dyadicGridCell G Q.1 Q.2, μ j y) : ‖∫ (y : ℝ) in dyadicGridCell G I.1 I.2, D n y * θ y‖ ≤ ‖∫ (y : ℝ) in dyadicGridCell G I.1 I.2, μ n y * θ y‖ + ∑ j ∈ Finset.Ico n (n + d), 2 * L * 2⁻¹ ^ j * √(dyadicGridLength G I.1) * (√(∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖D j y - D (j + 1) y‖ ^ 2) + √(∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖μ (j + 1) y - μ j y‖ ^ 2)) + L * 2⁻¹ ^ (n + d) * √(dyadicGridLength G I.1) * √(∫ (y : ℝ) in dyadicGridCell G I.1 I.2, ‖D (n + d) y‖ ^ 2)

Blueprint lem:delay, eq:delay-telescope, as an estimate on one cell I of depth s: D_j, μ_j are the residual and its predictor moment at depth s + j (so ∫_Q D_j = ∫_Q μ_j and μ_j is constant on the depth-(s+j) cells Q ⊆ I), and θ is a bump with ‖θ‖ ≤ L and Lipschitz constant L/|I|. The telescoping is stopped at depth s + n + d.

theorem TrilinearHT.Auto.weighted_sq_sum_le {ι : Type u_1} (s : Finset ι) (c a : ι → ℝ) (hc : ∀ j ∈ s, 0 ≤ c j) : (∑ j ∈ s, c j * a j) ^ 2 ≤ (∑ j ∈ s, c j) * ∑ j ∈ s, c j * a j ^ 2

Weighted Cauchy–Schwarz: (Σ c a)² ≤ (Σ c)(Σ c a²) for c ≥ 0.

theorem TrilinearHT.Auto.sum_depth_cells_le (G : RealDyadicGrid) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)) (s : ℤ) (hS : ∀ I ∈ S, I.1 = s ∧ dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) {F : ℝ → ℝ} (hF0 : ∀ (y : ℝ), 0 ≤ F y) (hF : MeasureTheory.IntegrableOn F (dyadicGridCell G J.1 J.2) MeasureTheory.volume) : ∑ I ∈ S, ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, F y ≤ ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, F y

Disjoint cells of one depth inside J carry at most the mass of J.

theorem TrilinearHT.Auto.sum_cells_energy_le (G : RealDyadicGrid) (J : ℤ × ℤ) (S : Finset (ℤ × ℤ)) (hSJ : ∀ I ∈ S, dyadicGridCell G I.1 I.2 ⊆ dyadicGridCell G J.1 J.2) (e : ℤ → ℝ → ℝ) (he0 : ∀ (h : ℤ) (y : ℝ), 0 ≤ e h y) (hei : ∀ (h : ℤ), MeasureTheory.IntegrableOn (e h) (dyadicGridCell G J.1 J.2) MeasureTheory.volume) {E : ℝ} (hE : ∀ (Hs : Finset ℤ), ∑ h ∈ Hs, ∫ (y : ℝ) in dyadicGridCell G J.1 J.2, e h y ≤ E) (j : ℕ) : ∑ I ∈ S, ∫ (y : ℝ) in dyadicGridCell G I.1 I.2, e (I.1 + ↑j) y ≤ E

The energy of all use cells at a fixed depth offset.

theorem TrilinearHT.Auto.sum_geom_inj_le {α : Type u_1} (T : Finset α) (g : α → ℕ) (hg : Set.InjOn g ↑T) : ∑ s ∈ T, 2⁻¹ ^ g s ≤ 2

theorem TrilinearHT.Auto.geom_Ico_le (K d : ℕ) : ∑ j ∈ Finset.Ico K (K + d), 2⁻¹ ^ j ≤ 2 * 2⁻¹ ^ K

theorem TrilinearHT.Auto.sqrt_setIntegral_le_of_le {s : Set ℝ} {u : ℝ → ℂ} {e : ℝ → ℝ} {c : ℝ} (hc : 0 ≤ c) (he : MeasureTheory.IntegrableOn e s MeasureTheory.volume) (hu : ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict s, ‖u y‖ ^ 2 ≤ c * e y) : √(∫ (y : ℝ) in s, ‖u y‖ ^ 2) ≤ √c * √(∫ (y : ℝ) in s, e y)