Finite element method in one dimension

DefinitionLength of a mesh element#✓fully proved

The length hᵢ = xᵢ₊₁ - xᵢ of the i-th element of the mesh.

noncomputable def width (i : Fin P.n) : ℝ :=
  P.points i.succ - P.points i.castSucc

Uses 1 · Used by 19

Statement usesPartition of an interval

Used byQuadratic form of the stiffness matrix · Slope of a P1 function on a mesh element · Weak form of the classical solution for P1 test functions · Stiffness matrix is the Gram matrix of the hat functions · Energy form of two P1 functions · Best approximation · Interpolation estimate · L² error estimate · Nodal values of the exact solution solve the Galerkin system · Uniqueness of the Galerkin solution · P1 functions are linear on each element · Linear map from nodal values to P1 functions · P1 functions interpolate their nodal values · Assembled stiffness matrix of the P1 method · Off-diagonal stiffness entry of an element · Tridiagonality of the stiffness matrix · Diagonal stiffness entry at an interior node · Element lengths are bounded by the mesh size · Mesh elements have positive length

DefinitionSlope of a P1 function on a mesh element#✓fully proved

The slope (dᵢ₊₁ - dᵢ) / hᵢ on the i-th element of the P1 function with nodal values d.

noncomputable def elementSlope (d : Fin (P.n + 1) → ℝ) (i : Fin P.n) : ℝ :=
  (d i.succ - d i.castSucc) / width P i

Uses 2 · Used by 14

Statement usesPartition of an interval · Length of a mesh element

Used byContinuity of P1 functions · Weak form of the classical solution for P1 test functions · Energy pairing with a P1 function via nodal differences · Energy form of two P1 functions · Best approximation · Interpolation estimate · Element-wise energy of a function minus a P1 function · Galerkin orthogonality · Derivative of a P1 function inside an element · L² error estimate · Nodal values of the exact solution solve the Galerkin system · Continuous piecewise linear function with given nodal values · P1 functions are linear on each element · P1 functions interpolate their nodal values

DefinitionClamped ramp function of a mesh element#✓fully proved

The clamped ramp of the i-th element: 0 left of xᵢ, x - xᵢ on [xᵢ, xᵢ₊₁], and hᵢ right of xᵢ₊₁.

noncomputable def ramp (i : Fin P.n) (x : ℝ) : ℝ :=
  max (P.points i.castSucc) (min x (P.points i.succ)) - P.points i.castSucc

Uses 1 · Used by 4

Statement usesPartition of an interval

Used byContinuity of P1 functions · Continuous piecewise linear function with given nodal values · P1 functions are linear on each element · Linear map from nodal values to P1 functions

DefinitionContinuous piecewise linear function with given nodal values#✓fully proved

The continuous piecewise linear (P1) function with nodal values d: d₀ + ∑ᵢ slopeᵢ · rampᵢ(x). On [0, 1] it is linear on each element and takes the value dⱼ at xⱼ; outside [0, 1] it is constant.

noncomputable def p1 (d : Fin (P.n + 1) → ℝ) (x : ℝ) : ℝ :=
  d 0 + ∑ i, elementSlope P d i * ramp P i x

Uses 3 · Used by 22

Statement usesPartition of an interval · Slope of a P1 function on a mesh element · Clamped ramp function of a mesh element

Used byContinuity of P1 functions · Weak form of the classical solution for P1 test functions · Stiffness matrix is the Gram matrix of the hat functions · Energy pairing with a P1 function via nodal differences · Energy form of two P1 functions · Best approximation · Energy error estimate · Interpolation estimate · Element-wise energy of a function minus a P1 function · Galerkin orthogonality · Derivative of a P1 function inside an element · Hat function of a mesh node · Interior hat functions lie in the P1 space · L² error estimate · Nodal interpolant of a function · Nodal values of the exact solution solve the Galerkin system · Characterization of membership in the P1 space · In one dimension the Galerkin solution is the nodal interpolant · P1 functions are linear on each element · Linear map from nodal values to P1 functions · P1 functions interpolate their nodal values · Energy error estimate for the P1 Galerkin solution

DefinitionHat function of a mesh node#✓fully proved

The hat function φⱼ of node j: the P1 function equal to 1 at xⱼ and 0 at every other node.

noncomputable def hat (j : Fin (P.n + 1)) : ℝ → ℝ :=
  p1 P (Pi.single j 1)

Uses 2 · Used by 4

Statement usesPartition of an interval · Continuous piecewise linear function with given nodal values

Used byStiffness matrix is the Gram matrix of the hat functions · Interior hat functions lie in the P1 space · Nodal values of the exact solution solve the Galerkin system · Load vector of the P1 method

DefinitionNodal interpolant of a function#✓fully proved

The nodal interpolant I_h u: the P1 function with nodal values u(xⱼ).

noncomputable def interp (u : ℝ → ℝ) : ℝ → ℝ :=
  p1 P fun j => u (P.points j)

Uses 2 · Used by 4

Statement usesPartition of an interval · Continuous piecewise linear function with given nodal values

Used byEnergy error estimate · Interpolation estimate · L² error estimate · In one dimension the Galerkin solution is the nodal interpolant

DefinitionLinear map from nodal values to P1 functions#✓fully proved

p1 as a linear map from nodal values to functions.

MathlibExt.Analysis.ODE.FiniteElement1D.p1Map · 16 lines

noncomputable def p1Map : (Fin (P.n + 1) → ℝ) →ₗ[ℝ] ℝ → ℝ where
  toFun := p1 P
  map_add' c d := by
    funext x
    simp only [p1, elementSlope, Pi.add_apply]
    rw [add_add_add_comm, ← Finset.sum_add_distrib]
    congr 1
    refine Finset.sum_congr rfl fun i _ => ?_
    ring
  map_smul' a d := by
    funext x
    simp only [p1, elementSlope, Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
    rw [mul_add, Finset.mul_sum]
    congr 1
    refine Finset.sum_congr rfl fun i _ => ?_
    ring

Uses 4 · Used by 2

Statement usesPartition of an interval · Continuous piecewise linear function with given nodal values · Clamped ramp function of a mesh element · Length of a mesh element

Used byCharacterization of membership in the P1 space · P1 finite element space with zero boundary values

DefinitionNodal vectors with zero boundary values#✓fully proved

Nodal vectors with zero boundary values d₀ = dₙ = 0.

def dirichletNodal : Submodule ℝ (Fin (P.n + 1) → ℝ) :=
  LinearMap.ker (LinearMap.proj 0) ⊓ LinearMap.ker (LinearMap.proj (Fin.last P.n))

Uses 1 · Used by 1

Statement usesPartition of an interval

Used byP1 finite element space with zero boundary values

DefinitionP1 finite element space with zero boundary values#✓fully proved

The P1 finite element space V_h with zero boundary values: the image under p1Map of the nodal vectors vanishing at both ends.

noncomputable def p1Space : Submodule ℝ (ℝ → ℝ) :=
  (dirichletNodal P).map (p1Map P)

Uses 3 · Used by 5

Statement usesPartition of an interval · Nodal vectors with zero boundary values · Linear map from nodal values to P1 functions

Used byWeak form of the classical solution for P1 test functions · Best approximation · Galerkin orthogonality · Interior hat functions lie in the P1 space · Characterization of membership in the P1 space

DefinitionEnergy form of the equation \(-u'' = f\)#✓fully proved

The energy form a(u, v) = ∫₀¹ u'(x) v'(x) dx of -u'' = f. For a P1 function, deriv is junk at the mesh nodes, a null set.

noncomputable def energy (u v : ℝ → ℝ) : ℝ :=
  ∫ x in (0 : ℝ)..1, deriv u x * deriv v x

Used by 12

Used byWeak form of the classical solution for \(C^1\) test functions · Weak form of the classical solution for P1 test functions · Stiffness matrix is the Gram matrix of the hat functions · Energy pairing with a P1 function via nodal differences · Energy form of two P1 functions · Best approximation · Energy error estimate · Interpolation estimate · Element-wise energy of a function minus a P1 function · Galerkin orthogonality · Nodal values of the exact solution solve the Galerkin system · Energy error estimate for the P1 Galerkin solution

DefinitionElement vector of the stiffness assembly#✓fully proved

The i-th element vector eᵢ = δ_{i+1} - δᵢ of the assembly.

noncomputable def elementVector (i : Fin P.n) : Fin (P.n + 1) → ℝ :=
  Pi.single i.succ 1 - Pi.single i.castSucc 1

Uses 1 · Used by 6

Statement usesPartition of an interval

Used byQuadratic form of the stiffness matrix · Stiffness matrix is the Gram matrix of the hat functions · Assembled stiffness matrix of the P1 method · Off-diagonal stiffness entry of an element · Tridiagonality of the stiffness matrix · Diagonal stiffness entry at an interior node

DefinitionAssembled stiffness matrix of the P1 method#✓fully proved

The assembled stiffness matrix K = ∑ᵢ (1 / hᵢ) eᵢ eᵢᵀ on all nodes: each element contributes (1 / hᵢ) [[1, -1], [-1, 1]] at nodes i, i + 1.

noncomputable def stiffness : Matrix (Fin (P.n + 1)) (Fin (P.n + 1)) ℝ :=
  fun j k => ∑ i, elementVector P i j * elementVector P i k / width P i

Uses 3 · Used by 8

Statement usesPartition of an interval · Element vector of the stiffness assembly · Length of a mesh element

Used byQuadratic form of the stiffness matrix · Stiffness matrix is the Gram matrix of the hat functions · Solution of the Galerkin system · Nodal values of the exact solution solve the Galerkin system · Uniqueness of the Galerkin solution · Off-diagonal stiffness entry of an element · Tridiagonality of the stiffness matrix · Diagonal stiffness entry at an interior node

DefinitionLoad vector of the P1 method#✓fully proved

The load vector Fⱼ = ∫₀¹ f φⱼ.

noncomputable def load (f : ℝ → ℝ) (j : Fin (P.n + 1)) : ℝ :=
  ∫ x in (0 : ℝ)..1, f x * hat P j x

Uses 2 · Used by 3

Statement usesPartition of an interval · Hat function of a mesh node

Used bySolution of the Galerkin system · Nodal values of the exact solution solve the Galerkin system · Uniqueness of the Galerkin solution

StructureClassical solution of the Dirichlet problem \(-u'' = f\)#✓fully proved

u is a classical solution of -u'' = f on (0, 1) with u(0) = u(1) = 0. We ask u to be C² on all of ℝ, which is no loss for the interval problem (a C² function on [0, 1] extends), and f to be continuous. The equation is stated on the open interval, as in the Dirichlet problem: requiring it at the endpoints without regularity of f would be a genuine strengthening. With f continuous, endpoint equality follows by continuity (eq_Icc), and the integral proofs use that derived version.

structure IsClassicalSolution (f u : ℝ → ℝ) : Prop where
  contDiff : ContDiff ℝ 2 u
  f_cont : Continuous f
  zero_left : u 0 = 0
  zero_right : u 1 = 0
  eq : ∀ x ∈ Set.Ioo (0 : ℝ) 1, -deriv (deriv u) x = f x

Used by 10

Used byWeak form of the classical solution for \(C^1\) test functions · Weak form of the classical solution for P1 test functions · Best approximation · Energy error estimate · Classical solutions satisfy the equation on the closed interval · Galerkin orthogonality · L² error estimate · Nodal values of the exact solution solve the Galerkin system · In one dimension the Galerkin solution is the nodal interpolant · Energy error estimate for the P1 Galerkin solution

TheoremClassical solutions satisfy the equation on the closed interval#✓fully proved

Endpoint equality, derived from the open-interval equation by continuity of -u'' and f: the two sides agree on (0, 1), hence on its closure [0, 1].

theorem IsClassicalSolution.eq_Icc {f u : ℝ → ℝ} (hu : IsClassicalSolution f u)
    {x : ℝ} (hx : x ∈ Set.Icc (0 : ℝ) 1) : -deriv (deriv u) x = f x

Uses 1 · Used by 4

Statement usesClassical solution of the Dirichlet problem \(-u'' = f\)

Used byWeak form of the classical solution for \(C^1\) test functions · Weak form of the classical solution for P1 test functions · Energy error estimate · L² error estimate

DefinitionSolution of the Galerkin system#✓fully proved

The coefficient vector c solves the Galerkin system: zero boundary values and (K c)ⱼ = Fⱼ at every interior node j. The Galerkin solution is u_h = p1 P c.

def IsGalerkinSolution (f : ℝ → ℝ) (c : Fin (P.n + 1) → ℝ) : Prop :=
  c 0 = 0 ∧ c (Fin.last P.n) = 0 ∧
    ∀ j, j ≠ 0 → j ≠ Fin.last P.n → (stiffness P).mulVec c j = load P f j

Uses 3 · Used by 8

Statement usesPartition of an interval · Load vector of the P1 method · Assembled stiffness matrix of the P1 method

Used byBest approximation · Energy error estimate · Galerkin orthogonality · L² error estimate · Nodal values of the exact solution solve the Galerkin system · Uniqueness of the Galerkin solution · In one dimension the Galerkin solution is the nodal interpolant · Energy error estimate for the P1 Galerkin solution

46 fully proved

The P1 functions

TheoremMesh elements have positive length#✓fully proved

Every element has positive length.

theorem width_pos (i : Fin P.n) : 0 < width P i

Uses 2 · Used by 6

Statement usesPartition of an interval · Length of a mesh element

Used byWeak form of the classical solution for P1 test functions · Best approximation · Interpolation estimate · L² error estimate · Uniqueness of the Galerkin solution · P1 functions are linear on each element

TheoremElement lengths are bounded by the mesh size#✓fully proved

Every element length is at most the mesh size h.

theorem width_le_mesh (i : Fin P.n) : width P i ≤ P.mesh

Uses 3 · Used by 2

Statement usesPartition of an interval · Mesh of a partition · Length of a mesh element

Used byInterpolation estimate · L² error estimate

TheoremP1 functions are linear on each element#✓fully proved

On the i-th element, p1 P d is the linear function through (xᵢ, dᵢ) with slope slopeᵢ = elementSlope P d i.

theorem p1_eq_of_mem_Icc (d : Fin (P.n + 1) → ℝ) (i : Fin P.n) {x : ℝ}
    (hx : x ∈ Set.Icc (P.points i.castSucc) (P.points i.succ)) :
    p1 P d x = d i.castSucc + elementSlope P d i * (x - P.points i.castSucc)

Uses 6 · Used by 4

Statement usesPartition of an interval · Slope of a P1 function on a mesh element · Continuous piecewise linear function with given nodal values

Proof usesClamped ramp function of a mesh element · Length of a mesh element · Mesh elements have positive length

Used byWeak form of the classical solution for P1 test functions · Derivative of a P1 function inside an element · L² error estimate · P1 functions interpolate their nodal values

TheoremP1 functions interpolate their nodal values#✓fully proved

p1 P d interpolates the nodal values.

theorem p1_points (d : Fin (P.n + 1) → ℝ) (j : Fin (P.n + 1)) :
    p1 P d (P.points j) = d j

Uses 6 · Used by 2

Statement usesPartition of an interval · Continuous piecewise linear function with given nodal values

Proof usesA partition of a nondegenerate interval has a subinterval · Slope of a P1 function on a mesh element · P1 functions are linear on each element · Length of a mesh element

Used byEnergy form of two P1 functions · Galerkin orthogonality

TheoremContinuity of P1 functions#✓fully proved

P1 functions are continuous.

theorem continuous_p1 (d : Fin (P.n + 1) → ℝ) : Continuous (p1 P d)

Uses 4 · Used by 3

Statement usesPartition of an interval · Continuous piecewise linear function with given nodal values

Proof usesSlope of a P1 function on a mesh element · Clamped ramp function of a mesh element

Used byEnergy form of two P1 functions · Galerkin orthogonality · L² error estimate

TheoremDerivative of a P1 function inside an element#✓fully proved

Inside an element, p1 P d has derivative slopeᵢ.

theorem hasDerivAt_p1 (d : Fin (P.n + 1) → ℝ) (i : Fin P.n) {x : ℝ}
    (hx : x ∈ Set.Ioo (P.points i.castSucc) (P.points i.succ)) :
    HasDerivAt (p1 P d) (elementSlope P d i) x

Uses 4 · Used by 4

Statement usesPartition of an interval · Slope of a P1 function on a mesh element · Continuous piecewise linear function with given nodal values

Proof usesP1 functions are linear on each element

Used byEnergy pairing with a P1 function via nodal differences · Energy form of two P1 functions · Element-wise energy of a function minus a P1 function · Galerkin orthogonality

TheoremIntegral over the unit interval as a sum over elements#✓fully proved

An integral over [0, 1] is the sum of the integrals over the elements.

theorem integral_eq_sum (g : ℝ → ℝ)
    (hg : ∀ i : Fin P.n, IntervalIntegrable g volume (P.points i.castSucc) (P.points i.succ)) :
    ∫ x in (0 : ℝ)..1, g x = ∑ i : Fin P.n, ∫ x in P.points i.castSucc..P.points i.succ, g x

Uses 1 · Used by 5

Statement usesPartition of an interval

Used byWeak form of the classical solution for P1 test functions · Energy pairing with a P1 function via nodal differences · Interpolation estimate · Element-wise energy of a function minus a P1 function · L² error estimate

TheoremEnergy pairing with a P1 function via nodal differences#✓fully proved

The key identity of the 1D P1 method: for w continuous on each element, differentiable inside it, and with integrable derivative there, a(w, p1 d) = ∑ᵢ slopeᵢ(d) (w(xᵢ₊₁) - w(xᵢ)).

theorem energy_p1 (w : ℝ → ℝ)
    (hcont : ∀ i : Fin P.n, ContinuousOn w (Set.Icc (P.points i.castSucc) (P.points i.succ)))
    (hdiff : ∀ i : Fin P.n, ∀ x ∈ Set.Ioo (P.points i.castSucc) (P.points i.succ),
      DifferentiableAt ℝ w x)
    (hint : ∀ i : Fin P.n,
      IntervalIntegrable (deriv w) volume (P.points i.castSucc) (P.points i.succ))
    (d : Fin (P.n + 1) → ℝ) :
    energy w (p1 P d) =
      ∑ i, elementSlope P d i * (w (P.points i.succ) - w (P.points i.castSucc))

Uses 6 · Used by 4

Statement usesPartition of an interval · Slope of a P1 function on a mesh element · Energy form of the equation \(-u'' = f\) · Continuous piecewise linear function with given nodal values

Proof usesDerivative of a P1 function inside an element · Integral over the unit interval as a sum over elements

Used byWeak form of the classical solution for P1 test functions · Energy form of two P1 functions · Galerkin orthogonality · Nodal values of the exact solution solve the Galerkin system

Weak form, stiffness matrix, Galerkin orthogonality

TheoremCharacterization of membership in the P1 space#✓fully proved

Membership in the P1 space: v = p1 P d for nodal values d with d₀ = dₙ = 0.

theorem mem_p1Space {v : ℝ → ℝ} :
    v ∈ p1Space P ↔ ∃ d, d 0 = 0 ∧ d (Fin.last P.n) = 0 ∧ p1 P d = v

Uses 4 · Used by 4

Statement usesPartition of an interval · Continuous piecewise linear function with given nodal values · P1 finite element space with zero boundary values

Proof usesLinear map from nodal values to P1 functions

Used byWeak form of the classical solution for P1 test functions · Best approximation · Galerkin orthogonality · Interior hat functions lie in the P1 space

TheoremInterior hat functions lie in the P1 space#✓fully proved

The hat function of an interior node lies in the P1 space.

theorem hat_mem_p1Space {j : Fin (P.n + 1)} (h0 : j ≠ 0) (hl : j ≠ Fin.last P.n) :
    hat P j ∈ p1Space P

Uses 5 · Used by 1

Statement usesPartition of an interval · Hat function of a mesh node · P1 finite element space with zero boundary values

Proof usesCharacterization of membership in the P1 space · Continuous piecewise linear function with given nodal values

Used byNodal values of the exact solution solve the Galerkin system

TheoremWeak form of the classical solution for \(C^1\) test functions#✓fully proved

The weak form for C¹ test functions vanishing at 0 and 1: ∫₀¹ u' v' = ∫₀¹ f v.

theorem energy_eq_integral_mul_of_contDiff {f u v : ℝ → ℝ} (hu : IsClassicalSolution f u)
    (hv : ContDiff ℝ 1 v) (hv0 : v 0 = 0) (hv1 : v 1 = 0) :
    energy u v = ∫ x in (0 : ℝ)..1, f x * v x

Uses 3

Statement usesClassical solution of the Dirichlet problem \(-u'' = f\) · Energy form of the equation \(-u'' = f\)

Proof usesClassical solutions satisfy the equation on the closed interval

TheoremWeak form of the classical solution for P1 test functions#✓fully proved

The weak form for P1 test functions: ∫₀¹ u' v_h' = ∫₀¹ f v_h.

theorem energy_eq_integral_mul_of_mem_p1Space {f u v : ℝ → ℝ} (hu : IsClassicalSolution f u)
    (hv : v ∈ p1Space P) :
    energy u v = ∫ x in (0 : ℝ)..1, f x * v x

Uses 13 · Used by 1

Statement usesPartition of an interval · Classical solution of the Dirichlet problem \(-u'' = f\) · Energy form of the equation \(-u'' = f\) · P1 finite element space with zero boundary values

Proof usesClassical solutions satisfy the equation on the closed interval · Slope of a P1 function on a mesh element · Energy pairing with a P1 function via nodal differences · Integral over the unit interval as a sum over elements · Characterization of membership in the P1 space · Continuous piecewise linear function with given nodal values · P1 functions are linear on each element · Length of a mesh element · Mesh elements have positive length

Used byNodal values of the exact solution solve the Galerkin system

TheoremEnergy form of two P1 functions#✓fully proved

The energy form of two P1 functions: a(p1 c, p1 d) = ∑ᵢ (cᵢ₊₁ - cᵢ)(dᵢ₊₁ - dᵢ) / hᵢ.

theorem energy_p1_p1 (c d : Fin (P.n + 1) → ℝ) :
    energy (p1 P c) (p1 P d) =
      ∑ i, (c i.succ - c i.castSucc) * (d i.succ - d i.castSucc) / width P i

Uses 9 · Used by 1

Statement usesPartition of an interval · Energy form of the equation \(-u'' = f\) · Continuous piecewise linear function with given nodal values · Length of a mesh element

Proof usesContinuity of P1 functions · Slope of a P1 function on a mesh element · Energy pairing with a P1 function via nodal differences · Derivative of a P1 function inside an element · P1 functions interpolate their nodal values

Used byStiffness matrix is the Gram matrix of the hat functions

TheoremQuadratic form of the stiffness matrix#✓fully proved

The quadratic form of the stiffness matrix: dᵀ K c = ∑ᵢ (cᵢ₊₁ - cᵢ)(dᵢ₊₁ - dᵢ) / hᵢ.

theorem dotProduct_stiffness_mulVec (c d : Fin (P.n + 1) → ℝ) :
    d ⬝ᵥ (stiffness P).mulVec c =
      ∑ i, (c i.succ - c i.castSucc) * (d i.succ - d i.castSucc) / width P i

Uses 4 · Used by 2

Statement usesPartition of an interval · Assembled stiffness matrix of the P1 method · Length of a mesh element

Proof usesElement vector of the stiffness assembly

Used byNodal values of the exact solution solve the Galerkin system · Uniqueness of the Galerkin solution

TheoremStiffness matrix is the Gram matrix of the hat functions#✓fully proved

The stiffness matrix is the Gram matrix of the hat functions: a(φⱼ, φₖ) = Kⱼₖ.

theorem energy_hat_hat (j k : Fin (P.n + 1)) :
    energy (hat P j) (hat P k) = stiffness P j k

Uses 8

Statement usesPartition of an interval · Energy form of the equation \(-u'' = f\) · Hat function of a mesh node · Assembled stiffness matrix of the P1 method

Proof usesElement vector of the stiffness assembly · Energy form of two P1 functions · Continuous piecewise linear function with given nodal values · Length of a mesh element

TheoremOff-diagonal stiffness entry of an element#✓fully proved

The off-diagonal entry of an element: K_{i, i+1} = -1 / hᵢ.

theorem stiffness_castSucc_succ (i : Fin P.n) :
    stiffness P i.castSucc i.succ = -(width P i)⁻¹

Uses 4

Statement usesPartition of an interval · Assembled stiffness matrix of the P1 method · Length of a mesh element

Proof usesElement vector of the stiffness assembly

TheoremDiagonal stiffness entry at an interior node#✓fully proved

The diagonal entry at an interior node xⱼ shared by consecutive elements i and j: K = 1 / hᵢ + 1 / hⱼ.

theorem stiffness_succ_succ {i j : Fin P.n} (hij : i.succ = j.castSucc) :
    stiffness P i.succ i.succ = (width P i)⁻¹ + (width P j)⁻¹

Uses 4

Statement usesPartition of an interval · Assembled stiffness matrix of the P1 method · Length of a mesh element

Proof usesElement vector of the stiffness assembly

TheoremTridiagonality of the stiffness matrix#✓fully proved

Entries between nodes two or more apart vanish (tridiagonality).

theorem stiffness_eq_zero {j k : Fin (P.n + 1)} (hjk : (j : ℕ) + 2 ≤ k) :
    stiffness P j k = 0

Uses 4

Statement usesPartition of an interval · Assembled stiffness matrix of the P1 method

Proof usesElement vector of the stiffness assembly · Length of a mesh element

TheoremNodal values of the exact solution solve the Galerkin system#✓fully proved

The nodal values of the exact solution solve the Galerkin system.

theorem isGalerkinSolution_nodal {f u : ℝ → ℝ} (hu : IsClassicalSolution f u) :
    IsGalerkinSolution P f fun j => u (P.points j)

Uses 14 · Used by 3

Statement usesPartition of an interval · Classical solution of the Dirichlet problem \(-u'' = f\) · Solution of the Galerkin system

Proof usesQuadratic form of the stiffness matrix · Slope of a P1 function on a mesh element · Energy form of the equation \(-u'' = f\) · Weak form of the classical solution for P1 test functions · Energy pairing with a P1 function via nodal differences · Hat function of a mesh node · Interior hat functions lie in the P1 space · Load vector of the P1 method · Continuous piecewise linear function with given nodal values · Assembled stiffness matrix of the P1 method · Length of a mesh element

Used byBest approximation · Galerkin orthogonality · In one dimension the Galerkin solution is the nodal interpolant

TheoremUniqueness of the Galerkin solution#✓fully proved

The Galerkin system has at most one solution (K is positive definite on nodal vectors with zero boundary values).

theorem isGalerkinSolution_unique {f : ℝ → ℝ} {c c' : Fin (P.n + 1) → ℝ}
    (hc : IsGalerkinSolution P f c) (hc' : IsGalerkinSolution P f c') : c = c'

Uses 7 · Used by 3

Statement usesPartition of an interval · Solution of the Galerkin system

Proof usesQuadratic form of the stiffness matrix · Load vector of the P1 method · Assembled stiffness matrix of the P1 method · Length of a mesh element · Mesh elements have positive length

Used byBest approximation · Galerkin orthogonality · In one dimension the Galerkin solution is the nodal interpolant

TheoremIn one dimension the Galerkin solution is the nodal interpolant#✓fully proved

In one dimension the P1 Galerkin solution is the nodal interpolant of the exact solution: u_h = I_h u.

theorem p1_eq_interp_of_isGalerkinSolution {f u : ℝ → ℝ} (hu : IsClassicalSolution f u)
    {c : Fin (P.n + 1) → ℝ} (hc : IsGalerkinSolution P f c) :
    p1 P c = interp P u

Uses 7 · Used by 2

Statement usesPartition of an interval · Classical solution of the Dirichlet problem \(-u'' = f\) · Solution of the Galerkin system · Nodal interpolant of a function · Continuous piecewise linear function with given nodal values

Proof usesNodal values of the exact solution solve the Galerkin system · Uniqueness of the Galerkin solution

Used byEnergy error estimate · L² error estimate

TheoremGalerkin orthogonality#✓fully proved

a(u - u_h, v_h) = 0 for every v_h ∈ V_h.

theorem galerkin_orthogonality {f u : ℝ → ℝ} (hu : IsClassicalSolution f u)
    {c : Fin (P.n + 1) → ℝ} (hc : IsGalerkinSolution P f c) {v : ℝ → ℝ}
    (hv : v ∈ p1Space P) :
    energy (u - p1 P c) v = 0

Uses 14

Statement usesPartition of an interval · Classical solution of the Dirichlet problem \(-u'' = f\) · Solution of the Galerkin system · Energy form of the equation \(-u'' = f\) · Continuous piecewise linear function with given nodal values · P1 finite element space with zero boundary values

Proof usesContinuity of P1 functions · Slope of a P1 function on a mesh element · Energy pairing with a P1 function via nodal differences · Derivative of a P1 function inside an element · Nodal values of the exact solution solve the Galerkin system · Uniqueness of the Galerkin solution · Characterization of membership in the P1 space · P1 functions interpolate their nodal values

TheoremElement-wise energy of a function minus a P1 function#✓fully proved

Element-wise form of the energy of u - p1 d for a C² function u: a(u - p1 d, u - p1 d) = ∑ᵢ ∫_{xᵢ}^{xᵢ₊₁} (u' - slopeᵢ(d))².

theorem energy_sub_p1_self {u : ℝ → ℝ} (hu : ContDiff ℝ 2 u)
    (d : Fin (P.n + 1) → ℝ) :
    energy (u - p1 P d) (u - p1 P d) = ∑ i, ∫ x in P.points i.castSucc..P.points i.succ,
      (deriv u x - elementSlope P d i) ^ 2

Uses 6 · Used by 2

Statement usesPartition of an interval · Slope of a P1 function on a mesh element · Energy form of the equation \(-u'' = f\) · Continuous piecewise linear function with given nodal values

Proof usesDerivative of a P1 function inside an element · Integral over the unit interval as a sum over elements

Used byBest approximation · Interpolation estimate

TheoremBest approximation#✓fully proved

Best approximation (Céa's lemma for the symmetric energy form, with constant 1): ‖u - u_h‖_a ≤ ‖u - v_h‖_a for every v_h ∈ V_h.

theorem energy_sub_galerkin_le {f u : ℝ → ℝ} (hu : IsClassicalSolution f u)
    {c : Fin (P.n + 1) → ℝ} (hc : IsGalerkinSolution P f c) {v : ℝ → ℝ}
    (hv : v ∈ p1Space P) :
    energy (u - p1 P c) (u - p1 P c) ≤ energy (u - v) (u - v)

Uses 13

Statement usesPartition of an interval · Classical solution of the Dirichlet problem \(-u'' = f\) · Solution of the Galerkin system · Energy form of the equation \(-u'' = f\) · Continuous piecewise linear function with given nodal values · P1 finite element space with zero boundary values

Proof usesSlope of a P1 function on a mesh element · Element-wise energy of a function minus a P1 function · Nodal values of the exact solution solve the Galerkin system · Uniqueness of the Galerkin solution · Characterization of membership in the P1 space · Length of a mesh element · Mesh elements have positive length

Error estimates

TheoremWirtinger's inequality on an interval#✓fully proved

Wirtinger's inequality on [a, b]: a C¹ function vanishing at a and b satisfies ∫ₐᵇ g² ≤ ((b - a) / π)² ∫ₐᵇ (g')².

theorem integral_sq_le_of_eq_zero {g : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hg : ContDiff ℝ 1 g)
    (ha : g a = 0) (hb : g b = 0) :
    ∫ x in a..b, g x ^ 2 ≤ ((b - a) / Real.pi) ^ 2 * ∫ x in a..b, deriv g x ^ 2

Uses 1 · Used by 2

Proof usesWirtinger's inequality

Used byElement estimate for \(C^2\) functions vanishing at both ends · L² error estimate

TheoremElement estimate for \(C^2\) functions vanishing at both ends#✓fully proved

The element estimate: a C² function vanishing at a and b satisfies ∫ₐᵇ (g')² ≤ ((b - a) / π)² ∫ₐᵇ (g'')².

theorem integral_deriv_sq_le_of_eq_zero {g : ℝ → ℝ} {a b : ℝ} (hab : a < b)
    (hg : ContDiff ℝ 2 g) (ha : g a = 0) (hb : g b = 0) :
    ∫ x in a..b, deriv g x ^ 2 ≤
      ((b - a) / Real.pi) ^ 2 * ∫ x in a..b, deriv (deriv g) x ^ 2

Uses 1 · Used by 2

Proof usesWirtinger's inequality on an interval

Used byInterpolation estimate · L² error estimate

TheoremInterpolation estimate#✓fully proved

‖u - I_h u‖_a² ≤ (h / π)² ‖u''‖²_{L²(0,1)}, with h the mesh size.

theorem energy_sub_interp_le {u : ℝ → ℝ} (hu : ContDiff ℝ 2 u) :
    energy (u - interp P u) (u - interp P u) ≤
      (P.mesh / Real.pi) ^ 2 * ∫ x in (0 : ℝ)..1, deriv (deriv u) x ^ 2

Uses 12 · Used by 1

Statement usesPartition of an interval · Mesh of a partition · Energy form of the equation \(-u'' = f\) · Nodal interpolant of a function

Proof usesSlope of a P1 function on a mesh element · Element-wise energy of a function minus a P1 function · Element estimate for \(C^2\) functions vanishing at both ends · Integral over the unit interval as a sum over elements · Continuous piecewise linear function with given nodal values · Length of a mesh element · Element lengths are bounded by the mesh size · Mesh elements have positive length

Used byEnergy error estimate

TheoremEnergy error estimate#✓fully proved

‖u - u_h‖_a² ≤ (h / π)² ‖f‖²_{L²(0,1)}, so the energy error is O(h).

theorem energy_sub_galerkin_le_mesh {f u : ℝ → ℝ} (hu : IsClassicalSolution f u)
    {c : Fin (P.n + 1) → ℝ} (hc : IsGalerkinSolution P f c) :
    energy (u - p1 P c) (u - p1 P c) ≤
      (P.mesh / Real.pi) ^ 2 * ∫ x in (0 : ℝ)..1, f x ^ 2

Uses 10 · Used by 1

Statement usesPartition of an interval · Mesh of a partition · Classical solution of the Dirichlet problem \(-u'' = f\) · Solution of the Galerkin system · Energy form of the equation \(-u'' = f\) · Continuous piecewise linear function with given nodal values

Proof usesClassical solutions satisfy the equation on the closed interval · Interpolation estimate · Nodal interpolant of a function · In one dimension the Galerkin solution is the nodal interpolant

Used byEnergy error estimate for the P1 Galerkin solution

TheoremEnergy error estimate for the P1 Galerkin solution#✓fully proved

The energy error estimate in norm form: ‖u - u_h‖_a ≤ (h / π) ‖f‖_{L²(0,1)}.

theorem sqrt_energy_sub_galerkin_le_mesh {f u : ℝ → ℝ} (hu : IsClassicalSolution f u)
    {c : Fin (P.n + 1) → ℝ} (hc : IsGalerkinSolution P f c) :
    √(energy (u - p1 P c) (u - p1 P c)) ≤
      P.mesh / Real.pi * √(∫ x in (0 : ℝ)..1, f x ^ 2)

Uses 8

Statement usesPartition of an interval · Mesh of a partition · Classical solution of the Dirichlet problem \(-u'' = f\) · Solution of the Galerkin system · Energy form of the equation \(-u'' = f\) · Continuous piecewise linear function with given nodal values

Proof usesThe mesh is positive on a nondegenerate interval · Energy error estimate

TheoremL² error estimate#✓fully proved

‖u - u_h‖²_{L²(0,1)} ≤ (h / π)⁴ ‖f‖²_{L²(0,1)}, so the L² error is O(h²). The proof uses nodal exactness and Wirtinger's inequality on each element, not the Aubin–Nitsche duality argument.

theorem integral_sq_sub_galerkin_le_mesh {f u : ℝ → ℝ} (hu : IsClassicalSolution f u)
    {c : Fin (P.n + 1) → ℝ} (hc : IsGalerkinSolution P f c) :
    ∫ x in (0 : ℝ)..1, (u x - p1 P c x) ^ 2 ≤
      (P.mesh / Real.pi) ^ 4 * ∫ x in (0 : ℝ)..1, f x ^ 2

Uses 17

Statement usesPartition of an interval · Mesh of a partition · Classical solution of the Dirichlet problem \(-u'' = f\) · Solution of the Galerkin system · Continuous piecewise linear function with given nodal values

Proof usesClassical solutions satisfy the equation on the closed interval · Continuity of P1 functions · Slope of a P1 function on a mesh element · Element estimate for \(C^2\) functions vanishing at both ends · Integral over the unit interval as a sum over elements · Wirtinger's inequality on an interval · Nodal interpolant of a function · In one dimension the Galerkin solution is the nodal interpolant · P1 functions are linear on each element · Length of a mesh element · Element lengths are bounded by the mesh size · Mesh elements have positive length

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.