CellSymbols.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Cell restrictions inside original endpoint symbols

An indicator in the spatial variable leaves the restricted transform unchanged and requires no spatial derivative. It makes all nonstationary geometry hypotheses conditional on genuinely active point labels.

def OAI.Falconer.cellSymbol line 19
theorem OAI.Falconer.cellSymbol_measurable line 23
theorem OAI.Falconer.cellSymbol_active line 28
theorem OAI.Falconer.cellSymbol_bound line 34
theorem OAI.Falconer.endpointTransform_cellSymbol line 42
theorem OAI.Falconer.cellSymbol_chart_smooth line 53
theorem OAI.Falconer.capPair_cell_active line 66

theorem OAI.Falconer.cellCapPair_displacement_bounds line 76

Source documentation

The phase bounds refer to the actual descendant cubes whenever there is a nonzero cap amplitude.

theorem cellCapPair_displacement_bounds {d n : ℕ}
    (Q : DyadicCube d) (hQ : 0 < Q.side) (p q : List (Fin d → Bool))
    (hp : p.length = n) (hq : q.length = n)
    (η : Sphere d → ℝ) (b b' : Space d → Sphere d → ℂ)
    (x : Space d × Space d) {δ : ℝ} (hδ : 0 ≤ δ)
    (hactive : ∃ w, capPairAmplitude η (cellSymbol (Q.descendant p) b)
      (cellSymbol (Q.descendant q) b') x w ≠ 0) :
    ‖x.1-x.2‖ ≤ Real.sqrt d*Q.side ∧
    ‖(x.1-x.2)-((Q.descendant p).center-(Q.descendant q).center)‖ +
      8*δ*‖(Q.descendant p).center-(Q.descendant q).center‖ ≤
        2*Real.sqrt d*(Q.side/(2 : ℝ)^n)+8*δ*(Real.sqrt d*Q.side) := by
…

Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Sphere, OAI.Falconer.Space, OAI.Falconer.capPairAmplitude, OAI.Falconer.cellSymbol

theorem OAI.Falconer.endpointCapCrossTerm_cellSymbols line 92