ShiftedBlocks.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

The actual shifted block endpoints of §8. The first block is allowed to be shorter. Every transition has one phase tag, and each completed block contains its distinguished phase exactly at the last transition.

def OAI.LipschitzHilbert.ShiftedBlocks.endpoint line 17
theorem OAI.LipschitzHilbert.ShiftedBlocks.endpoint_zero line 21
theorem OAI.LipschitzHilbert.ShiftedBlocks.endpoint_succ line 23
theorem OAI.LipschitzHilbert.ShiftedBlocks.endpoint_strictMono line 26
def OAI.LipschitzHilbert.ShiftedBlocks.block line 33
def OAI.LipschitzHilbert.ShiftedBlocks.lastTransition line 36
theorem OAI.LipschitzHilbert.ShiftedBlocks.lastTransition_eq line 38
theorem OAI.LipschitzHilbert.ShiftedBlocks.lastTransition_succ line 44
theorem OAI.LipschitzHilbert.ShiftedBlocks.endpoint_first_bounds line 49
theorem OAI.LipschitzHilbert.ShiftedBlocks.endpoint_step line 54
theorem OAI.LipschitzHilbert.ShiftedBlocks.endpoint_width_le line 59
theorem OAI.LipschitzHilbert.ShiftedBlocks.block_card_first line 65
theorem OAI.LipschitzHilbert.ShiftedBlocks.block_card_succ line 68
theorem OAI.LipschitzHilbert.ShiftedBlocks.block_card_le line 74
theorem OAI.LipschitzHilbert.ShiftedBlocks.lastTransition_mem line 81
theorem OAI.LipschitzHilbert.ShiftedBlocks.block_nonempty line 88
theorem OAI.LipschitzHilbert.ShiftedBlocks.block_disjoint_of_lt line 91
theorem OAI.LipschitzHilbert.ShiftedBlocks.blocks_pairwiseDisjoint line 101
def OAI.LipschitzHilbert.ShiftedBlocks.tag line 109
Source documentation
The phase coordinate of a transition in the shared analytic family.
```
def tag (hK : 0 < K) (i : ℕ) : Fin K := ⟨i % K, Nat.mod_lt i hK⟩
```
theorem OAI.LipschitzHilbert.ShiftedBlocks.tag_val line 111
theorem OAI.LipschitzHilbert.ShiftedBlocks.tag_lastTransition line 113
theorem OAI.LipschitzHilbert.ShiftedBlocks.endpoint_tag_div line 118
theorem OAI.LipschitzHilbert.ShiftedBlocks.endpoint_eq_last_sub line 126
Source documentation
The block ending at transition i starts at the source's shared boundary ancestor i+1-K, with truncated subtraction at the root.
```
theorem endpoint_eq_last_sub (σ : Fin K) (j : ℕ) :
    endpoint σ j = lastTransition σ j + 1 - K := by
…
```
Mentions: OAI.LipschitzHilbert.ShiftedBlocks.endpoint, OAI.LipschitzHilbert.ShiftedBlocks.lastTransition
theorem OAI.LipschitzHilbert.ShiftedBlocks.block_start_tag_div line 137
theorem OAI.LipschitzHilbert.ShiftedBlocks.is_last_iff_tag line 144
theorem OAI.LipschitzHilbert.ShiftedBlocks.tag_injective_on_block line 156
theorem OAI.LipschitzHilbert.ShiftedBlocks.tag_eq_shift_iff line 167
theorem OAI.LipschitzHilbert.ShiftedBlocks.prod_block_eq_last line 176
theorem OAI.LipschitzHilbert.ShiftedBlocks.packetPathProduct_norm_eq_last line 183

theorem OAI.LipschitzHilbert.ShiftedBlocks.analytic_block_norm line 197

Source documentation

At a vertex parameter, the modulus of a complete block product is the modulus contributed by its final transition alone. Other phase coordinates may still have arbitrary imaginary parts.

theorem analytic_block_norm (hK : 0 < K) (σ : Fin K) (j : ℕ)
    (g : AngularGrid) (mass boundary : ℕ → ℤ → ℝ) (phase : Fin K → ℂ) (slope : ℝ)
    (hphase : ∀ τ, τ ≠ σ → (phase τ).re = 0)
    (hm : ∀ i ∈ block σ j, 0 < mass (i + 1) (g.index (i + 1) slope))
    (hb : ∀ i ∈ block σ j, 0 < boundary i (g.index (i + 1) slope)) :
    ‖g.packetPathProduct (AngularGrid.analyticTransition mass boundary (fun i => phase (tag hK i)))
      (endpoint σ j) (endpoint σ (j + 1)) slope‖ =
      (mass (endpoint σ (j + 1)) (g.index (endpoint σ (j + 1)) slope) /
        boundary (lastTransition σ j) (g.index (endpoint σ (j + 1)) slope)) ^ (phase σ).re := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.ShiftedBlocks.block, OAI.LipschitzHilbert.AngularGrid.analyticTransition, OAI.LipschitzHilbert.ShiftedBlocks.tag, OAI.LipschitzHilbert.ShiftedBlocks.endpoint, OAI.LipschitzHilbert.ShiftedBlocks.lastTransition