SourceResidualSplit.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact short/long splitting of the source residual. A packet at least as long as the reference top cannot stop before an eligible reference endpoint. The long part is therefore confined to the last block and its square costs only its one terminal envelope.

theorem OAI.LipschitzHilbert.AngularGrid.packetResidual_filter_split line 19
theorem OAI.LipschitzHilbert.AngularGrid.residual_packet_length_lt line 31

theorem OAI.LipschitzHilbert.AngularGrid.long_packet_residual_eq_zero line 50

Source documentation

The physical long-packet residual vanishes at every block whose upper endpoint is still eligible for the distinguished reference top.

theorem long_packet_residual_eq_zero (g : AngularGrid) (packets : Finset σ)
    (slope length : σ → ℝ) (hlen : ∀ q, 0 < length q)
    {w B referenceLength : ℝ} (hw : 0 < w) (hB : 0 < B) (hR : 0 < referenceLength)
    (hzero : ∀ q ∈ packets, g.eligible (g.rootWidth/B^2) (w/length q) 0)
    (base : σ → E) (transition : ℕ → ℤ → ℂ) (lower upper : ℕ) (cell : ℤ)
    (hreference : g.eligible (g.rootWidth/B^2) (w/referenceLength) upper) :
    g.packetResidual (packets.filter fun q => ¬length q ≤ referenceLength) slope
      (fun q => g.lastEligible (g.rootWidth/B^2) (w/length q) (div_pos hw (hlen q)))
      base transition lower upper cell = 0 := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.source_residual_short_long line 68
theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_long_residual_support line 83

theorem OAI.LipschitzHilbert.terminal_perturbation_square_sum line 104

Source documentation

Adding a term supported at the last block has no depth loss.

theorem terminal_perturbation_square_sum {E : Type*} [NormedAddCommGroup E]
    {count : ℕ} (hc : 0 < count) (full short long : Fin count → E)
    (hsplit : ∀ j, full j = short j+long j)
    (hsupport : ∀ j : Fin count, j.val+1 < count → long j = 0)
    {P R : ℝ} (hshort : (∑ j, ‖short j‖^2) ≤ P)
    (hR : 0 ≤ R) (hterminal : ‖long ⟨count-1,by omega⟩‖ ≤ R) :
    (∑ j, ‖full j‖^2) ≤ 2*P+2*R^2 := by
…