ScalarCancellation1.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SignedDisk.ScalarCancellation.scalar_defect_sum line 26

theorem OAI.SignedDisk.ScalarCancellation.errors_total_cost line 43

Source documentation

The total cancellation cost of all levels is bounded by the actual scalar input mass, independently of the number of refinement levels.

theorem errors_total_cost (w : ℕ → ι → ι → ℝ) (hw : ∀ k q s, 0 ≤ w k q s)
    (hcol : ∀ k s, ∑ q, w k q s = 1) {f : ι → α → ℝ}
    (hf : ∀ q, Integrable (f q) μ) (n : ℕ) :
    (∑ k ∈ range (n+1), ∑ q, ∫ x, |errors μ w f k q x| ∂μ) +
      (∑ q, |∫ x, refined w f n q x ∂μ|) ≤ ∑ q, ∫ x, |f q x| ∂μ := by
…

Mentions: OAI.SignedDisk.ScalarCancellation.errors, OAI.SignedDisk.ScalarCancellation.refined

lemma OAI.SignedDisk.ScalarCancellation.errors_total_cost_le line 57

theorem OAI.SignedDisk.ScalarCancellation.telescoped_decomposition line 68

Source documentation

Exact expansion in a coherent family of refinement coefficients. The finite zero-mass pieces are the explicitly constructed errors, not merely scalar mass certificates.

theorem telescoped_decomposition [DecidableEq ι] (w : ℕ → ι → ι → ℝ) (f : ι → α → ℝ)
    (Λ : ℕ → ℕ → ι → ι → ℝ)
    (hdiag : ∀ k q s, Λ k k q s = if q = s then 1 else 0)
    (hstep : ∀ k j q s, j ≤ k → Λ (k+1) j q s = ∑ a, w k q a*Λ k j a s)
    (k : ℕ) (q : ι) (x : α) :
    refined w f k q x = roots μ w f k q x +
      ∑ j ∈ range (k+1), ∑ s, Λ k j q s*errors μ w f j s x := by
…

Mentions: OAI.SignedDisk.ScalarCancellation.refined, OAI.SignedDisk.ScalarCancellation.roots, OAI.SignedDisk.ScalarCancellation.errors

def OAI.SignedDisk.DyadicHats.tent line 113
lemma OAI.SignedDisk.DyadicHats.tent_nonneg line 115
lemma OAI.SignedDisk.DyadicHats.tent_le_one line 116
lemma OAI.SignedDisk.DyadicHats.tent_pos_iff line 117
lemma OAI.SignedDisk.DyadicHats.tent_eq_zero_of_one_le line 123
lemma OAI.SignedDisk.DyadicHats.tent_of_nonneg line 125
lemma OAI.SignedDisk.DyadicHats.tent_of_nonpos line 127
lemma OAI.SignedDisk.DyadicHats.tent_neg line 130
lemma OAI.SignedDisk.DyadicHats.lipschitz_tent line 132
theorem OAI.SignedDisk.DyadicHats.tent_refine line 141
lemma OAI.SignedDisk.DyadicHats.tent_floor line 166
lemma OAI.SignedDisk.DyadicHats.tent_floor_succ line 168
lemma OAI.SignedDisk.DyadicHats.tent_floor_partition line 171
lemma OAI.SignedDisk.DyadicHats.tent_eq_zero_of_ne_floor line 174
lemma OAI.SignedDisk.DyadicHats.summable_tent line 186
theorem OAI.SignedDisk.DyadicHats.tsum_tent line 193
Source documentation
Partition of unity on the complete integer grid, including grid boundaries.
```
theorem tsum_tent (x : ℝ) : (∑' j : ℤ, tent (x-j)) = 1 := by
…
```
Mentions: OAI.SignedDisk.DyadicHats.tent
def OAI.SignedDisk.DyadicHats.hat line 201
Source documentation
Actual Euclidean-plane product hats at a positive physical scale.
```
def hat (r : ℝ) (p : ℤ × ℤ) (x : ℂ) : ℝ :=
…
```
lemma OAI.SignedDisk.DyadicHats.hat_nonneg line 203
lemma OAI.SignedDisk.DyadicHats.hat_le_one line 205
lemma OAI.SignedDisk.DyadicHats.continuous_hat line 209
lemma OAI.SignedDisk.DyadicHats.summable_hat line 214
theorem OAI.SignedDisk.DyadicHats.tsum_hat line 218
lemma OAI.SignedDisk.DyadicHats.tent_half_integer line 224
Source documentation
One-dimensional refinement written with the actual interpolation weights.
```
lemma tent_half_integer {j : ℤ} (hj : j ∉ Finset.Icc (-1) 1) : tent ((j:ℝ)/2) = 0 := by
…
```
Mentions: OAI.SignedDisk.DyadicHats.tent
lemma OAI.SignedDisk.DyadicHats.tent_half_refine line 235
lemma OAI.SignedDisk.DyadicHats.tent_half_tsum_refine line 247
lemma OAI.SignedDisk.DyadicHats.summable_tent_weight line 263
def OAI.SignedDisk.DyadicHats.step line 271
Source documentation
Positive interpolation coefficients, indexed by coarse and fine grid indices.
```
def step (p q : ℤ × ℤ) : ℝ :=
…
```
lemma OAI.SignedDisk.DyadicHats.step_nonneg line 273
lemma OAI.SignedDisk.DyadicHats.step_column line 275
lemma OAI.SignedDisk.DyadicHats.summable_step_hat line 283
theorem OAI.SignedDisk.DyadicHats.hat_refine line 294
Source documentation
Exact planar hat refinement; no grid truncation is hidden in the identity.
```
theorem hat_refine (r : ℝ) (p : ℤ × ℤ) (x : ℂ) :
    hat (2*r) p x = ∑' q : ℤ × ℤ, step p q*hat r q x := by
…
```
Mentions: OAI.SignedDisk.DyadicHats.hat, OAI.SignedDisk.DyadicHats.step
lemma OAI.SignedDisk.PlanePotential.dim_complex line 318
lemma OAI.SignedDisk.PlanePotential.volume_real_unit_ball line 320
lemma OAI.SignedDisk.PlanePotential.integral_radial line 324
lemma OAI.SignedDisk.PlanePotential.integrable_radial_iff line 331
lemma OAI.SignedDisk.PlanePotential.radial_near_identity line 336
lemma OAI.SignedDisk.PlanePotential.integrable_norm_rpow_near line 343
theorem OAI.SignedDisk.PlanePotential.integral_norm_rpow_near line 356
Source documentation
Exact planar singular-kernel integral; the center point is not excluded by an unproved integrability convention.
```
theorem integral_norm_rpow_near {a r : ℝ} (ha : -2 < a) (hr : 0 < r) :
    (∫ x in ball (0:ℂ) r, ‖x‖^a) = 2*Real.pi * (r^(a+2)/(a+2)) := by
…
```
lemma OAI.SignedDisk.PlanePotential.radial_far_identity line 372
lemma OAI.SignedDisk.PlanePotential.integrable_norm_rpow_far line 379
theorem OAI.SignedDisk.PlanePotential.integral_norm_rpow_far line 393