High-contrast homogenization: Provider.Response.RowCellEnergyBound

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The per-scale cell-energy bound of a cutoff-defect mean row

The scale sums of a cutoff-defect mean row weigh each aligned cell by the terminal optimizer's energy on that cell. Because the aligned cells of one scale partition their parent with equal volume, the normalized average of those cell energies is exactly the terminal response value; after annealing, the normalized average of the annealed cell energies is exactly the annealed terminal response.

The row is written on the cells of the reference scale-s cell, so each row cell carries the annealed energy averaged over the scale-s parents in which it sits; the parent average and the within-parent average then compose to the single average over the terminal cell.

The pathwise cell energy

noncomputable def HCPolySupport.HighContrast.Response.cellQuarterEnergy {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) (p r : Vec d) : ℝ

The pathwise quarter energy of the terminal optimizer state on an aligned cell. The quarter normalizes the doubled energy density to the response value: the normalized average over one aligned subdivision is exactly the terminal response.

Equations

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

theorem HCPolySupport.HighContrast.Response.avsum_cellQuarterEnergy_eq_responseJ {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) (a : CoeffSpace d) (p r : Vec d) : (avsum (alignedIndex q k t) fun (w : Fin d → ℤ) => cellQuarterEnergy hq k t w a p r) = Book.Ch02.responseJ (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) p r

The equal-volume parent-energy partition. The normalized average of the pathwise quarter cell energies over one aligned subdivision of the terminal cell is exactly the terminal response value.

The annealed cell energy

noncomputable def HCPolySupport.HighContrast.Response.profileAnnealedCellEnergySq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) (w : Fin d → ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) : ℝ

The annealed quarter energy of the terminal optimizer state on an aligned cell.

Equations

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

theorem HCPolySupport.HighContrast.Response.avsum_profileAnnealedCellEnergySq_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (hint : ∀ w ∈ alignedIndex q k t, MeasureTheory.Integrable (fun (a : CoeffSpace d) => cellQuarterEnergy hq k t w (sample a) p r) P) : (avsum (alignedIndex q k t) fun (w : Fin d → ℤ) => profileAnnealedCellEnergySq P hq k t w sample p r) = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((sample a).coeffOn (adaptedDomain hq t)) p r ∂P

The annealed parent-energy partition. The normalized average of the annealed quarter cell energies over one aligned subdivision of the terminal cell is exactly the annealed terminal response.

The row cell energy

def HCPolySupport.HighContrast.Response.nestedLabel {d : ℕ} (k s : ℤ) (z w : Fin d → ℤ) : Fin d → ℤ

The label of the scale-k cell sitting at relative position w inside the scale-s cell of label z.

Equations

• HCPolySupport.HighContrast.Response.nestedLabel k s z w i = 3 ^ (s - k).toNat * z i + w i

noncomputable def HCPolySupport.HighContrast.Response.profileRowCellEnergy {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (k s t : ℤ) (w : Fin d → ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) : ℝ

The annealed row cell energy: the energy the row closers weigh each reference cell by, averaged over the scale-s parents that carry a copy of that cell.

Equations

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

theorem HCPolySupport.HighContrast.Response.profileRowCellEnergy_nonneg {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (k s t : ℤ) (w : Fin d → ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) : 0 ≤ profileRowCellEnergy P hq k s t w sample p r

theorem HCPolySupport.HighContrast.Response.avsum_sq_profileRowCellEnergy_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) {k s t : ℤ} (hks : k ≤ s) (hst : s ≤ t) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (hnonneg : ∀ w ∈ alignedIndex q k t, 0 ≤ profileAnnealedCellEnergySq P hq k t w sample p r) (hnestMem : ∀ w ∈ alignedIndex q k s, ∀ z ∈ alignedIndex q s t, nestedLabel k s z w ∈ alignedIndex q k t) (hnest : ∀ (f : (Fin d → ℤ) → ℝ), (avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => avsum (alignedIndex q s t) fun (z : Fin d → ℤ) => f (nestedLabel k s z w)) = avsum (alignedIndex q k t) f) (hint : ∀ w ∈ alignedIndex q k t, MeasureTheory.Integrable (fun (a : CoeffSpace d) => cellQuarterEnergy hq k t w (sample a) p r) P) : (avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => profileRowCellEnergy P hq k s t w sample p r ^ 2) = ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((sample a).coeffOn (adaptedDomain hq t)) p r ∂P

The per-scale row energy identity. Under the nested reindexing of the aligned cells and the cellwise law integrability, the normalized average of the squared row cell energies at one scale is exactly the annealed terminal response.

The row closers' per-scale energy premise

theorem HCPolySupport.HighContrast.Response.sqrt_avsum_sq_profileRowCellEnergy_le {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (Klo s t : ℤ) (hst : s ≤ t) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (hnonneg : ∀ k ∈ Finset.Icc Klo s, ∀ w ∈ alignedIndex q k t, 0 ≤ profileAnnealedCellEnergySq P hq k t w sample p r) (hnestMem : ∀ k ∈ Finset.Icc Klo s, ∀ w ∈ alignedIndex q k s, ∀ z ∈ alignedIndex q s t, nestedLabel k s z w ∈ alignedIndex q k t) (hnest : ∀ k ∈ Finset.Icc Klo s, ∀ (f : (Fin d → ℤ) → ℝ), (avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => avsum (alignedIndex q s t) fun (z : Fin d → ℤ) => f (nestedLabel k s z w)) = avsum (alignedIndex q k t) f) (hint : ∀ k ∈ Finset.Icc Klo s, ∀ w ∈ alignedIndex q k t, MeasureTheory.Integrable (fun (a : CoeffSpace d) => cellQuarterEnergy hq k t w (sample a) p r) P) (k : ℤ) : k ∈ Finset.Icc Klo s → √(avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => profileRowCellEnergy P hq k s t w sample p r ^ 2) ≤ √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((sample a).coeffOn (adaptedDomain hq t)) p r ∂P)

The per-scale energy premise of the row closers. At the annealed row cell energies the premise holds with equality at the annealed terminal response root.

theorem HCPolySupport.HighContrast.Response.sqrt_avsum_sq_profileRowCellEnergy_adjoint_le {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (Klo s t : ℤ) (hst : s ≤ t) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (hnonneg : ∀ k ∈ Finset.Icc Klo s, ∀ w ∈ alignedIndex q k t, 0 ≤ profileAnnealedCellEnergySq P hq k t w (fun (a : CoeffSpace d) => (sample a).transpose) p r) (hnestMem : ∀ k ∈ Finset.Icc Klo s, ∀ w ∈ alignedIndex q k s, ∀ z ∈ alignedIndex q s t, nestedLabel k s z w ∈ alignedIndex q k t) (hnest : ∀ k ∈ Finset.Icc Klo s, ∀ (f : (Fin d → ℤ) → ℝ), (avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => avsum (alignedIndex q s t) fun (z : Fin d → ℤ) => f (nestedLabel k s z w)) = avsum (alignedIndex q k t) f) (hint : ∀ k ∈ Finset.Icc Klo s, ∀ w ∈ alignedIndex q k t, MeasureTheory.Integrable (fun (a : CoeffSpace d) => cellQuarterEnergy hq k t w (sample a).transpose p r) P) (k : ℤ) : k ∈ Finset.Icc Klo s → √(avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => profileRowCellEnergy P hq k s t w (fun (a : CoeffSpace d) => (sample a).transpose) p r ^ 2) ≤ √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((sample a).transpose.coeffOn (adaptedDomain hq t)) p r ∂P)

The coefficient-transpose form of the per-scale energy premise: the transposed sample carries the adjoint optimizer state and the adjoint terminal response.