OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledCrossIdentity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The residual-square and unary-variation estimates use exactly the same original analyzing coefficients and alternate physical synthesis. The mask is applied to the synthesized vector, with no coefficient change.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalCrossPacketValue_zero line 21
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedValue_eq_cross line 33