Cubature.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Equal-mass two-point Gauss rule

The tensor product of this degree-three rule uses eight equal masses in each three-dimensional cell. Exact moment identities and fourth-derivative estimates control its error.

def OAI.ContinuumCoulomb.gaussAbscissa line 23
def OAI.ContinuumCoulomb.gaussTwoPoint line 25
theorem OAI.ContinuumCoulomb.gaussAbscissa_pos line 27
theorem OAI.ContinuumCoulomb.gaussAbscissa_sq line 31
theorem OAI.ContinuumCoulomb.gaussTwoPoint_moment line 36
Source documentation
Exactness for all four monomial moments needed in each coordinate.
```
theorem gaussTwoPoint_moment (k : ℕ) (hk : k ≤ 3) :
    gaussTwoPoint (fun x => x ^ k) = ∫ x : ℝ in (-1)..1, x ^ k := by
…
```
Mentions: OAI.ContinuumCoulomb.gaussTwoPoint

theorem OAI.ContinuumCoulomb.gaussTwoPoint_cubic line 46

Source documentation

Equal-weight quadrature integrates every cubic exactly.

theorem gaussTwoPoint_cubic (coefficient : Fin 4 → ℝ) :
    gaussTwoPoint (fun x => ∑ k : Fin 4, coefficient k * x ^ (k : ℕ)) =
      ∫ x : ℝ in (-1)..1, ∑ k : Fin 4, coefficient k * x ^ (k : ℕ) := by
…

Mentions: OAI.ContinuumCoulomb.gaussTwoPoint

theorem OAI.ContinuumCoulomb.gauss_cell_nodes line 65

Source documentation

In the centered cell of side h, the distinct nodes lie strictly inside.

theorem gauss_cell_nodes {h : ℝ} (hh : 0 < h) :
    -h / 2 < -(h / 2) * gaussAbscissa ∧
    -(h / 2) * gaussAbscissa < (h / 2) * gaussAbscissa ∧
    (h / 2) * gaussAbscissa < h / 2 := by
…

Mentions: OAI.ContinuumCoulomb.gaussAbscissa

theorem OAI.ContinuumCoulomb.eight_node_mass line 77
Source documentation
The eight masses sum to the uniform charge of a cell.
```
theorem eight_node_mass (rho h : ℝ) :
    (8 : ℝ) * (rho * h ^ 3 / 8) = rho * h ^ 3 := by ring
```
theorem OAI.ContinuumCoulomb.unit_node_mass line 81
Source documentation
The manuscript's scale choice makes each mass exactly 1 / λ.
```
theorem unit_node_mass {rho k : ℝ} (hrho : 0 < rho) (hk : 0 < k) :
    rho * (1 / k) ^ 3 / 8 = 1 / (8 * k ^ 3 / rho) := by
…
```
def OAI.ContinuumCoulomb.gaussNode line 86
Source documentation
The two normalized abscissae, indexed for the tensor-product rule.
```
def gaussNode (b : Fin 2) : ℝ := if b = 0 then -gaussAbscissa else gaussAbscissa
```
Mentions: OAI.ContinuumCoulomb.gaussAbscissa

theorem OAI.ContinuumCoulomb.gaussTensor3_moment line 89

Source documentation

The three-dimensional rule is exact for each needed tensor monomial.

theorem gaussTensor3_moment (degree : Fin 3 → ℕ) (hdegree : ∀ i, degree i ≤ 3) :
    (∑ node : Fin 3 → Fin 2, ∏ i : Fin 3, gaussNode (node i) ^ degree i) =
      ∏ i : Fin 3, ∫ x : ℝ in (-1)..1, x ^ degree i := by
…

Mentions: OAI.ContinuumCoulomb.gaussNode

theorem OAI.ContinuumCoulomb.gaussTensor3_mass line 101
Source documentation
Exactly eight equal masses are used in a three-dimensional cell.
```
theorem gaussTensor3_mass (rho h : ℝ) :
    (∑ _node : Fin 3 → Fin 2, rho * h ^ 3 / 8) = rho * h ^ 3 := by
…
```

theorem OAI.ContinuumCoulomb.gaussTwoPoint_remainder_bound line 108

Source documentation

Uniform cubic approximation controls the quadrature and integral errors separately, using the positivity and total mass of the rule.

theorem gaussTwoPoint_remainder_bound
    (f : ℝ → ℝ) (coefficient : Fin 4 → ℝ) {epsilon : ℝ}
    (hf : ContinuousOn f (Set.Icc (-1) 1))
    (happrox : ∀ x ∈ Set.Icc (-1) 1,
      |f x - ∑ k : Fin 4, coefficient k * x ^ (k : ℕ)| ≤ epsilon) :
    |gaussTwoPoint f - ∫ x : ℝ in (-1)..1, f x| ≤ 4 * epsilon := by
…

Mentions: OAI.ContinuumCoulomb.gaussTwoPoint

theorem OAI.ContinuumCoulomb.gaussTwoPoint_C4_error line 150

Source documentation

A genuine fourth-derivative error bound for the normalized cell. The coarse constant suffices for the manuscript's polynomial error budgets.

theorem gaussTwoPoint_C4_error (f : ℝ → ℝ) {C : ℝ} (hCnonneg : 0 ≤ C)
    (hf : ContDiffOn ℝ 4 f (Set.Icc (-1) 1))
    (hC : ∀ x ∈ Set.Icc (-1) 1,
      ‖iteratedDerivWithin 4 f (Set.Icc (-1) 1) x‖ ≤ C) :
    |gaussTwoPoint f - ∫ x : ℝ in (-1)..1, f x| ≤ (32 / 3 : ℝ) * C := by
…

Mentions: OAI.ContinuumCoulomb.gaussTwoPoint

def OAI.ContinuumCoulomb.gaussCell line 184
Source documentation
The equal-weight rule on an actual interval, with its physical weights.
```
def gaussCell (a b : ℝ) (f : ℝ → ℝ) : ℝ :=
…
```
theorem OAI.ContinuumCoulomb.gaussCell_C4_error line 190
Source documentation
Local fourth-derivative control gives the fifth-power cell error needed when the eight-node tensor rule is summed over a fine mesh. No smoothness outside the cell is assumed, which matters for the Coulomb kernel.
```
theorem gaussCell_C4_error (a b : ℝ) (hab : a < b) (f : ℝ → ℝ)
    {C : ℝ} (hCnonneg : 0 ≤ C) (hf : ContDiffOn ℝ 4 f (Set.Icc a b))
    (hC : ∀ x ∈ Set.Icc a b, ‖iteratedDerivWithin 4 f (Set.Icc a b) x‖ ≤ C) :
    |gaussCell a b f - ∫ x : ℝ in a..b, f x| ≤ C * (b - a) ^ 5 / 3 := by
…
```
Mentions: OAI.ContinuumCoulomb.gaussCell