SourcePathPhaseMotion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removal of the actual path phase in §9, pred:path-errors. The scalar phase costs only the off-path mass, including when it is zero.

theorem OAI.LipschitzHilbert.finite_rotated_off_path_motion line 15

Source documentation

Sum the individual numerator errors before removing the moving path phase. The two errors may have different sizes.

theorem finite_rotated_off_path_motion {ι E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℂ E]
    (s : Finset ι) (l : ι → ℝ) (W W' : ι → E)
    {lam lam' : ℂ} {q η K u : ℝ}
    (hlam : lam ≠ 0) (hq0 : 0 ≤ q) (hq1 : q < 1)
    (hη : 0 ≤ η) (hK : 0 ≤ K)
    (hweight : ‖lam'-lam‖ ≤ q*‖lam‖)
    (hsum : ∑ i ∈ s, l i ≤ u)
    (hW : ∀ i ∈ s, ‖W i‖ ≤ K*l i)
    (hmove : ∀ i ∈ s, ‖W' i-W i‖ ≤ η*K*l i) :
    ‖(scalarPhase lam')⁻¹ • (∑ i ∈ s, W' i) -
      (scalarPhase lam)⁻¹ • (∑ i ∈ s, W i)‖ ≤ (η+2*q)*K*u := by
…

Mentions: OAI.LipschitzHilbert.scalarPhase

theorem OAI.LipschitzHilbert.finite_rotated_off_path_motion_of_quotient line 61

Source documentation

Quotient form, matching the actual transition-product motion theorem.

theorem finite_rotated_off_path_motion_of_quotient {ι E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℂ E]
    (s : Finset ι) (l : ι → ℝ) (W W' : ι → E)
    {lam lam' : ℂ} {q η K u : ℝ}
    (hlam : lam ≠ 0) (hq0 : 0 ≤ q) (hq1 : q < 1)
    (hη : 0 ≤ η) (hK : 0 ≤ K)
    (hweight : ‖lam'/lam-1‖ ≤ q)
    (hsum : ∑ i ∈ s, l i ≤ u)
    (hW : ∀ i ∈ s, ‖W i‖ ≤ K*l i)
    (hmove : ∀ i ∈ s, ‖W' i-W i‖ ≤ η*K*l i) :
    ‖(scalarPhase lam')⁻¹ • (∑ i ∈ s, W' i) -
      (scalarPhase lam)⁻¹ • (∑ i ∈ s, W i)‖ ≤ (η+2*q)*K*u :=
…

Mentions: OAI.LipschitzHilbert.scalarPhase

theorem OAI.LipschitzHilbert.AngularGrid.source_block_scalar_phase_motion line 80

Source documentation

The actual source transition product supplies the phase estimate needed by the finite off-path sum lemma. No displaced good-point hypothesis enters.

theorem source_block_scalar_phase_motion {ι : Type*}
    (g : AngularGrid) (tops : Finset ι) (T : ι → SlopeBox)
    (w B K D : ℝ) (hw : 0 < w) (hB : 1 ≤ B) (hK : 0 < K) (hD : 0 ≤ D)
    (hwidth : ∀ t ∈ tops, B^2*w ≤ (T t).width)
    {Kb : ℕ} (hKb : 0 < Kb) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
    (h lower upper : ℕ) (hbase : h ≤ lower)
    (hgap : ∀ j ∈ Finset.Ico lower upper, 0 ≤ gap j ∧ gap j ≤ g.width h)
    (top : ι) (htop : top ∈ tops)
    (he : g.eligible (g.rootWidth/B^2) (w/(T top).length) upper)
    (sR : ℝ) (hs : g.index h (T top).slope = g.index h sR)
    (child : ℝ) (hchild : 0 < child) (hblock : g.width h ≤ B*child)
    (b : ℝ) (hb : |b| ≤ w/(child*Real.sqrt (g.branching:ℝ))) (z : ℝ × ℝ)
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.AngularGrid.width